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

fix: let $e now matches the whole letDecl, so specify kinds

Browse source
This commit is contained in:
Sebastian Ullrich 2019-12-30 16:50:03 +01:00 • committed by Leonardo de Moura
parent b24df456ed
commit eb2f26a71e
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/Lean/Elab/Quotation.lean
View file

@ -189,7 +189,7 @@ private def getHeadInfo (alt : Alt) : HeadInfo :=
let pat := alt.fst.head!;
let unconditional (rhsFn) := { HeadInfo . rhsFn := rhsFn };
-- variable pattern
if pat.isOfKind `Lean.Parser.Term.id then unconditional $ fun rhs => `(let $pat := discr; $rhs)
if pat.isOfKind `Lean.Parser.Term.id then unconditional $ fun rhs => `(let $pat:id := discr; $rhs)
-- wildcard pattern
else if pat.isOfKind `Lean.Parser.Term.hole then unconditional pure
-- quotation pattern
@ -218,13 +218,13 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
| _ => anti;
-- Splices should only appear inside a nullKind node, see next case
if isAntiquotSplice quoted then unconditional $ fun _ => throwError quoted "unexpected antiquotation splice"
else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn := fun rhs => `(let $anti := discr; $rhs) }
else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn := fun rhs => `(let $anti:id := discr; $rhs) }
else unconditional $ fun _ => throwError anti "syntax_match: antiquotation must be variable"
| _ =>
-- quotation is a single antiquotation splice => bind args array
if isAntiquotSplicePat quoted then
let anti := (quoted.getArg 0).getArg 1;
unconditional $ fun rhs => `(let $anti := Syntax.getArgs discr; $rhs)
unconditional $ fun rhs => `(let $anti:term := Syntax.getArgs discr; $rhs)
else
-- not an antiquotation: match head shape
let argPats := quoted.getArgs.map $ fun arg => Syntax.node `Lean.Parser.Term.stxQuot #[mkAtom "`(", arg, mkAtom ")"];