## Stream: general

### Topic: variable a problem

#### Kevin Buzzard (Mar 08 2018 at 21:21):

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?

#### Kevin Buzzard (Mar 08 2018 at 21:29):

So we have to wait for the parser refactoring?

#### Sebastian Ullrich (Mar 08 2018 at 21:37):

Yes

Last updated: May 06 2021 at 22:13 UTC