idris-1.3.3: test/tutorial002/expected.out
tutorial002.idr:41:25-29:
|
41 | Main.natToBin_lemma_1 = proof
| ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.
tutorial002.idr:48:18-22:
|
48 | parity_lemma_1 = proof
| ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.
tutorial002.idr:54:18-22:
|
54 | parity_lemma_2 = proof {
| ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.