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

feat: basic unexpanders for Exists & Sigma

Browse source 
A bit brittle and not quite complete, but probably good enough in practice
This commit is contained in:
Sebastian Ullrich 2021-02-04 11:04:37 +01:00
parent 545ed50f83
commit bdf7b15a41
1 changed files with 17 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Init/NotationExtra.lean
View file

@ -79,12 +79,26 @@ end Lean
open Lean
macro "∃" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
macro "∃ " xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
macro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Exists xs b
macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders `Sigma xs b
macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders `PSigma xs b
macro:35 xs:bracketedExplicitBinders "×" b:term:35 : term => expandBrackedBinders `Sigma xs b
macro:35 xs:bracketedExplicitBinders "×'" b:term:35 : term => expandBrackedBinders `PSigma xs b
macro:35 xs:bracketedExplicitBinders " × " b:term:35 : term => expandBrackedBinders `Sigma xs b
macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders `PSigma xs b
@[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)
| _ => throw ()
@[appUnexpander Sigma] def unexpandSigma : Lean.PrettyPrinter.Unexpander
| `(Sigma 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)
| _ => throw ()
syntax "funext " (colGt term:max)+ : tactic