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