git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/tutorial004/expected.out
12 lines 316 B history raw
1tutorial004.idr:46:14-18:
2 |
346 | plusredZ_S = proof {
4 | ~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7tutorial004.idr:53:14-18:
8 |
953 | plusredZ_Z = proof {
10 | ~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.