git.iko.soy/Idris-dev
on ca34dec help sign in
Idris-dev/test/reg017/expected
13 lines 401 B history raw
1reg017.idr:5:17-23:
2 |
35 | { default tactics { refine Refl; solve; } prfA : a = a } ->
4 | ~~~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7reg017.idr:8:17-23:
8 |
98 | { default tactics { refine Refl; solve; } prfBC : b = c } ->
10 | ~~~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.