6ea7869c6a
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. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| leanpkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||