git.iko.soy/Idris-dev
on master help sign in
Get rid of warnings in pruviloj test
88fd351Joomy Korkut
test/pruviloj001/expected−6
compare with master
unifiedsplit
@@ -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)
70pair = %runElab (do intros ; construct ; hypothesis ; hypothesis)
70pair = %runElab (do intros ; construct ; hypothesis ; hypothesis)
71
71
72data Even : Nat -> Type where
72data Even : Nat -> Type where
73− evenZ : Even Z
73+ EvenZ : Even Z
74− evenSS : Even n -> Even (S (S n))
74+ EvenSS : Even n -> Even (S (S n))
75
75
76even6 : Even 6
76even6 : Even 6
77even6 = %runElab (do construct ; construct ; construct ; construct ; skip)
77even6 = %runElab (do construct ; construct ; construct ; construct ; skip)