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

fix: unexpand pairs

Browse source
This commit is contained in:
Daniel Selsam 2021-07-29 15:04:03 -07:00 • committed by Sebastian Ullrich
parent 3309da8f1e
commit 9744b51c1b
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/NotationExtra.lean
View file

@ -111,9 +111,9 @@ macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBi
| _ => throw ()
@[appUnexpander Prod.mk] def unexpandProdMk : Lean.PrettyPrinter.Unexpander
| `(Prod.mk $x `(($y, $ys,*))) => `(($x, $y, $ys,*))
| `(Prod.mk $x $y) => `(($x, $y))
| _ => throw ()
| `(Prod.mk $x ($y, $ys,*)) => `(($x, $y, $ys,*))
| `(Prod.mk $x $y) => `(($x, $y))
| _ => throw ()
@[appUnexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
| `(ite $c $t $e) => `(if $c then $t else $e)