Zulip Chat Archive

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?

Sebastian Ullrich (Mar 08 2018 at 21:27):

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

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


Last updated: Aug 03 2023 at 10:10 UTC