variable a problem

Stream: general

[Kevin Buzzard]

This is presumably well-known but it has just bitten one of my undergraduates. They wrote have Ht2 : (a < nat.succ t) → (nat.succ t < c) → (a < c), in the middle of a tactic proof, with a,t,c nats, and get a type mismatch error: term a has type nat.succ t < c : Prop. Chris tells me that this is because you can't use have in a tactic proof with an implies sign and a variable a. That sounds like a bug to me. Is it officially not a bug though?

[Sebastian Ullrich]

Oh, it is https://github.com/leanprover/lean/issues/1822

[Kevin Buzzard]

So we have to wait for the parser refactoring?

[Sebastian Ullrich]

Yes