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

fix: unexpanders can't specify exact names

Browse source
This commit is contained in:
Daniel Selsam 2021-07-30 13:41:36 -07:00 • committed by Sebastian Ullrich
parent 5acdf48366
commit db4d33487a
1 changed files with 18 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/Init/NotationExtra.lean
View file

@ -94,56 +94,56 @@ macro:35 xs:bracketedExplicitBinders " × " b:term:35 : term => expandBrackedBi
macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders `PSigma xs b
@[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
| `(Unit.unit) => `(())
| `($(_)) => `(())
| _ => throw ()
@[appUnexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
| `(List.nil) => `([])
| _ => throw ()
| `($(_)) => `([])
| _ => throw ()
@[appUnexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
| `(List.cons $x []) => `([$x])
| `(List.cons $x [$xs,*]) => `([$x, $xs,*])
| `($(_) $x []) => `([$x])
| `($(_) $x [$xs,*]) => `([$x, $xs,*])
| _ => throw ()
@[appUnexpander List.toArray] def unexpandListToArray : Lean.PrettyPrinter.Unexpander
| `(List.toArray [$xs,*]) => `(#[$xs,*])
| `($(_) [$xs,*]) => `(#[$xs,*])
| _ => throw ()
@[appUnexpander Prod.mk] def unexpandProdMk : Lean.PrettyPrinter.Unexpander
| `(Prod.mk $x ($y, $ys,*)) => `(($x, $y, $ys,*))
| `(Prod.mk $x $y) => `(($x, $y))
| `($(_) $x ($y, $ys,*)) => `(($x, $y, $ys,*))
| `($(_) $x $y) => `(($x, $y))
| _ => throw ()
@[appUnexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
| `(ite $c $t $e) => `(if $c then $t else $e)
| `($(_) $c $t $e) => `(if $c then $t else $e)
| _ => throw ()
@[appUnexpander sorryAx] def unexpandSorryAx : Lean.PrettyPrinter.Unexpander
| `(sorryAx _) => `(sorry)
| `(sorryAx _ $b) => `(sorry)
| `($(_) _) => `(sorry)
| `($(_) _ $b) => `(sorry)
| _ => throw ()
@[appUnexpander Eq.ndrec] def unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
| `(Eq.ndrec $m $h) => `($h ▸ $m)
| `($(_) $m $h) => `($h ▸ $m)
| _ => throw ()
@[appUnexpander Eq.rec] def unexpandEqRec : Lean.PrettyPrinter.Unexpander
| `(Eq.rec $m $h) => `($h ▸ $m)
| `($(_) $m $h) => `($h ▸ $m)
| _ => throw ()
@[appUnexpander Exists] def unexpandExists : Lean.PrettyPrinter.Unexpander
| `(Exists fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
| `(Exists fun $x:ident => $b) => `(∃ $x:ident, $b)
| `(Exists fun ($x:ident : $t) => $b) => `(∃ ($x:ident : $t), $b)
| `($(_) fun $x:ident => ∃ $xs:binderIdent*, $b) => `(∃ $x:ident $xs:binderIdent*, $b)
| `($(_) fun $x:ident => $b) => `(∃ $x:ident, $b)
| `($(_) fun ($x:ident : $t) => $b) => `(∃ ($x:ident : $t), $b)
| _ => throw ()
@[appUnexpander Sigma] def unexpandSigma : Lean.PrettyPrinter.Unexpander
| `(Sigma fun ($x:ident : $t) => $b) => `(($x:ident : $t) × $b)
| `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) × $b)
| _ => throw ()
@[appUnexpander PSigma] def unexpandPSigma : Lean.PrettyPrinter.Unexpander
| `(PSigma fun ($x:ident : $t) => $b) => `(($x:ident : $t) ×' $b)
| `($(_) fun ($x:ident : $t) => $b) => `(($x:ident : $t) ×' $b)
| _ => throw ()
syntax "funext " (colGt term:max)+ : tactic