git.iko.soy/Idris-dev
on 19a87f3 help sign in
Idris-dev/test/proof001/expected
12 lines 352 B history raw
1test029.idr:29:25-29:
2 |
329 | simple.append_lemma_2 = proof {
4 | ~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7test029.idr:36:25-29:
8 |
936 | simple.append_lemma_1 = proof {
10 | ~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.