git.iko.soy/Idris-dev
on cd87fcd help sign in
Idris-dev/test/basic002/expected
13 lines 384 B history raw
1test006.idr:25:23-27:
2 |
325 | Main.parity_lemma_2 = proof {
4 | ~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7test006.idr:32:23-27:
8 |
932 | Main.parity_lemma_1 = proof {
10 | ~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.
13[False, True, False, True, False, True]