diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 0c24264dc2..2e9afa507a 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -224,7 +224,7 @@ stx.isAntiquot || stx.isIdent @[builtinTermParser] def seqRight := tparser! infixR " *> " 60 @[builtinTermParser] def map := tparser! infixR " <$> " 100 -@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.nonEmptySeq +@[builtinTermParser] def byTactic := parser!:maxPrec "by " >> Tactic.nonEmptySeq @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|" >> toggleInsideQuot funBinder >> ")" end Term diff --git a/tests/lean/run/new_frontend2.lean b/tests/lean/run/new_frontend2.lean index b6ddbd1786..4ba6c1684a 100644 --- a/tests/lean/run/new_frontend2.lean +++ b/tests/lean/run/new_frontend2.lean @@ -25,3 +25,9 @@ by { subst h₁; exact rfl } + +theorem ex : {α : Type} → {a b c : α} → a = b → b = c → a = c := +@by { + intro α a b c h₁ h₂; + exact Eq.trans h₁ h₂ +}