From 6ea7869c6a30e318be4dfe4fc95e59fd9efa41ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Sep 2021 17:23:06 -0700 Subject: [PATCH] chore: "fix" `<|>` notation declaration The `infix` declaration was generating a delaborator, but it is producing the invalid term ``` ConstantFunction.f myFun 3 <|> fun _ => ConstantFunction.f myFun 4 ``` It is invalid because the `macro_rules` for `<|>` is based on `binop_lazy%` which introduces the `fun _ =>` for us. I tried to use ``` notation:20 a:21 " <|> " b:20 => HOrElse.hOrElse a fun _ : Unit => b ``` but the delaborator generator does not work for this case. --- src/Init/Notation.lean | 2 +- tests/lean/eagerCoeExpansion.lean.expected.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index aa4537ffb5..19a60c9f67 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -128,7 +128,7 @@ infixl:30 " || " => or notation:max "!" b:40 => not b infixr:67 " :: " => List.cons -infixr:20 " <|> " => HOrElse.hOrElse +syntax:20 term:21 " <|> " term:20 : term infixr:60 " >> " => HAndThen.hAndThen infixl:55 " >>= " => Bind.bind infixl:60 " <*> " => Seq.seq diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out index 8bd74e2eeb..ab4180aa42 100644 --- a/tests/lean/eagerCoeExpansion.lean.expected.out +++ b/tests/lean/eagerCoeExpansion.lean.expected.out @@ -22,4 +22,4 @@ fun (a : Nat) => (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) true) def s : Option Nat := -ConstantFunction.f myFun 3 <|> ConstantFunction.f myFun 4 +HOrElse.hOrElse (ConstantFunction.f myFun 3) fun x => ConstantFunction.f myFun 4