max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: reduce priority of old if-then-else parser

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-30 20:31:54 -07:00
parent ef4becfedb
commit 7ea23a0f37
1 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Notation.lean
View file

@ -137,15 +137,9 @@ infixr:100 " <$> " => Functor.map
macro_rules | `($x <|> $y) => `(binop_lazy% HOrElse.hOrElse $x $y)
macro_rules | `($x >> $y) => `(binop_lazy% HAndThen.hAndThen $x $y)
syntax (name := termDepIfThenElse) (priority := high) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
syntax (name := termDepIfThenElse) (priority := low) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
macro_rules
| `(if $h:ident : $c then $t:term else $e:term) => ``(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
syntax (name := termIfThenElse) (priority := high) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
macro_rules
| `(if $c then $t:term else $e:term) => ``(ite $c $t $e)
syntax (name := termIfThenElse) (priority := low) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
macro "if " "let " pat:term " := " d:term " then " t:term " else " e:term : term =>
`(match $d:term with | $pat:term => $t | _ => $e)