on 5e2000e help sign in
6 lines 182 B history raw
1ClaimAndUnfocus.idr:8:27-31:
2 |
38 | ClaimAndUnfocus.foo_rhs = proof
4 | ~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.