From 20152c11920709cd8fa904d82eee9e5bad457262 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Sep 2020 10:45:47 -0700 Subject: [PATCH] chore: change `by` precedence @Kha it now uses the same precedence of `fun`. The main motivation is to allow us to write `@by { ... }` instead of `@(by { ... })`. BTW, I am considering disabling implicit lambdas for `by ...` expressions. It is automatically "intro"ducing the implicit variables without giving an opportunity for users to pick their names. --- src/Lean/Parser/Term.lean | 2 +- tests/lean/run/new_frontend2.lean | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) 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₂ +}