git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/test/tutorial002/expected
18 lines 508 B history raw
1tutorial002.idr:41:25-29:
2 |
341 | Main.natToBin_lemma_1 = proof
4 | ~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7tutorial002.idr:48:18-22:
8 |
948 | parity_lemma_1 = proof
10 | ~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.
13tutorial002.idr:54:18-22:
14 |
1554 | parity_lemma_2 = proof {
16 | ~~~~~
17This style of tactic proof is deprecated. See %runElab for the replacement.