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

feat: unexpander for mkArray0

Browse source
This commit is contained in:
Mario Carneiro 2022-10-13 22:20:53 -04:00 • committed by Leonardo de Moura
parent dab88ae943
commit 0acdaddcf2
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/NotationExtra.lean
View file

@ -242,6 +242,9 @@ syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosi
| `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"]
| _ => throw ()
@[appUnexpander Array.mkArray0] def unexpandMkArray0 : Lean.PrettyPrinter.Unexpander
| _ => `(#[])
@[appUnexpander Array.mkArray1] def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander
| `($(_) $a1) => `(#[$a1])
| _ => throw ()

3
tests/lean/ppNotationCode.lean.expected.out
View file

@ -67,8 +67,7 @@
{ raw :=
Lean.Syntax.node info `Lean.Parser.Term.app
#[Lean.Syntax.node info `term_+++_ #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw],
Lean.Syntax.node info `null
(Array.append Array.mkArray0 (Lean.TSyntaxArray.raw moreArgs))] }.raw
Lean.Syntax.node info `null (Array.append #[] (Lean.TSyntaxArray.raw moreArgs))] }.raw
else
let_fun __discr_5 := Lean.Syntax.getArg __discr_2 1;
let_fun __discr := Lean.Syntax.getArg __discr 1;