From 85cda05c92abb3ed42a595a68b5322e6ce78f65e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Aug 2022 10:01:32 -0700 Subject: [PATCH] chore: improve `expandParen` do notation --- src/Lean/Elab/BuiltinNotation.lean | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 071f412d42..d61b686cc5 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -243,13 +243,17 @@ where /-- - Try to expand `·` notation. - Recall that in Lean the `·` notation must be surrounded by parentheses. - We may change this is the future, but right now, here are valid examples - - `(· + 1)` - - `(f ⟨·, 1⟩ ·)` - - `(· + ·)` - - `(f · a b)` -/ +You can use parentheses for +- Grouping expressions, e.g., `a * (b + c)`. +- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`. +- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`. +- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`. +- Creating simple functions when combined with `·`. Here are some examples: + - `(· + 1)` is shorthand for `fun x => x + 1` + - `(· + ·)` is shorthand for `fun x y => x + y` + - `(f · a b)` is shorthand for `fun x => f x a b` + - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x` +-/ @[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro | `(()) => `(Unit.unit) | `(($e : $type)) => do