git.iko.soy/Idris-dev
on dff4fcd help sign in
Idris-dev/test/reg044/expected
16 lines 405 B history raw
1reg044.idr:4:6-11:
2This style of tactic proof is deprecated. See %runElab for the replacement.
3reg044.idr:4:4:
4When checking right hand side of Main.pf with expected type
5 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
7Type mismatch between
8 b = b (Type of Refl)
9and
10 a = b (Expected type)
12Specifically:
13 Type mismatch between
14 b
15 and
16 a