| 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 |