git.iko.soy/Idris-dev
on 5e2000e help sign in
Idris-dev/test/proof003/expected
39 lines 1.0 kB history raw
1Parity.idr:17:18-22:
2 |
317 | parity_lemma_2 = proof {
4 | ~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7Parity.idr:24:18-22:
8 |
924 | parity_lemma_1 = proof {
10 | ~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.
13test015.idr:88:15-19:
14 |
1588 | Main.ntbOdd = proof {
16 | ~~~~~
17This style of tactic proof is deprecated. See %runElab for the replacement.
19test015.idr:97:16-20:
20 |
2197 | Main.ntbEven = proof {
22 | ~~~~~
23This style of tactic proof is deprecated. See %runElab for the replacement.
25test015.idr:107:20-24:
26 |
27107 | Main.adc_lemma_2 = proof {
28 | ~~~~~
29This style of tactic proof is deprecated. See %runElab for the replacement.
31test015.idr:142:20-24:
32 |
33142 | Main.adc_lemma_1 = proof {
34 | ~~~~~
35This style of tactic proof is deprecated. See %runElab for the replacement.
3700101010
3801011001
39010000011