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

fix: avoid notation in quotation elaborator output

Browse source
This commit is contained in:
Sebastian Ullrich 2023-01-19 14:39:39 +01:00
parent 18297d8d91
commit 8a4059dc65
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Quotation.lean
View file

@ -458,9 +458,9 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
| _ => undecided
doMatch := fun yes no => do
let prefixDiscrs ← (List.range idx).mapM (`(Syntax.getArg __discr $(quote ·)))
let sliceDiscr ← `(mkNullNode (__discr.getArgs.extract $(quote idx) (__discr.getNumArgs - $(quote numSuffix))))
let sliceDiscr ← `(mkNullNode (__discr.getArgs.extract $(quote idx) (Nat.sub __discr.getNumArgs $(quote numSuffix))))
let suffixDiscrs ← (List.range numSuffix).mapM fun i =>
`(Syntax.getArg __discr (__discr.getNumArgs - $(quote (numSuffix - i))))
`(Syntax.getArg __discr (Nat.sub __discr.getNumArgs $(quote (numSuffix - i))))
`(ite (GE.ge __discr.getNumArgs $(quote (quoted.getNumArgs - 1)))
$(← yes (prefixDiscrs ++ sliceDiscr :: suffixDiscrs))
$(← no))

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

@ -62,7 +62,7 @@
let_fun __discr_4 := Lean.Syntax.getArg __discr_3 1;
let_fun __discr_5 :=
Lean.mkNullNode
(Array.extract (Lean.Syntax.getArgs __discr_3) 2 (Lean.Syntax.getNumArgs __discr_3 - 0));
(Array.extract (Lean.Syntax.getArgs __discr_3) 2 (Nat.sub (Lean.Syntax.getNumArgs __discr_3) 0));
let_fun moreArgs := Lean.TSyntaxArray.mk (Lean.Syntax.getArgs __discr_5);
let_fun rhs := { raw := __discr_4 };
let_fun lhs := { raw := __discr };