You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
macro (priority := high) "let " x:ident : tactic => `(let' $x := ?_)
example : True := bylet x
exact Nat
-- expected ':=' or '|'
This is a regression caused by #1658, even though it was intended to improve the situation for exactly this example. (Perhaps the mathlib let/have should be defined in a test case...) It works if you put (let x) in parens but as written it gets parsed as let x exact Nat where exact and Nat are identifiers, followed by a parse error because the := is missing. As you can see, priority := high makes no difference for the parse.
The text was updated successfully, but these errors were encountered:
This is a regression caused by #1658, even though it was intended to improve the situation for exactly this example. (Perhaps the mathlib
let
/have
should be defined in a test case...) It works if you put(let x)
in parens but as written it gets parsed aslet x exact Nat
whereexact
andNat
are identifiers, followed by a parse error because the:=
is missing. As you can see,priority := high
makes no difference for the parse.The text was updated successfully, but these errors were encountered: