Get rid of warnings in pruviloj test
commit88fd351bce2202c964c3c6cb6c7d6f2f0fb4855d
authorJoomy Korkut <joomy@cattheory.com>
dateWed 4 Oct 2017, 07:39 (9 years ago)
parent954d858
test/pruviloj001/expected−6
@@ -1,6 +0,0 @@
1−pruviloj001.idr:73:9:
2−Main.evenZ has a name which may be implicitly bound.
3−This is likely to lead to problems!
4−pruviloj001.idr:74:10:
5−Main.evenSS has a name which may be implicitly bound.
6−This is likely to lead to problems!
test/pruviloj001/pruviloj001.idr+2−2
@@ -70,8 +70,8 @@ pair : a -> b -> (a, b)
7070pair = %runElab (do intros ; construct ; hypothesis ; hypothesis)
7171
7272data Even : Nat -> Type where
73− evenZ : Even Z
74− evenSS : Even n -> Even (S (S n))
73+ EvenZ : Even Z
74+ EvenSS : Even n -> Even (S (S n))
7575
7676even6 : Even 6
7777even6 = %runElab (do construct ; construct ; construct ; construct ; skip)