blob: e140ce8246431cb24cf5d2068a5e4ab2a1f18f02 [file] [edit]
issue3232.lean:5:2-5:9: error: tactic 'apply' failed, failed to unify
@foo 42
with
@foo 23
h : foo
⊢ foo
issue3232.lean:8:2-8:29: error: tactic 'apply' failed, failed to unify
(1 : Int) = 1
with
(1 : Nat) = 1
⊢ 1 = 1
issue3232.lean:11:2-11:25: error: tactic 'apply' failed, failed to unify
PUnit = PUnit
with
PUnit = PUnit
⊢ PUnit = PUnit