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

refactor: replace mkTermIdFromIdent with antiquotation kind where possible

Browse source
This commit is contained in:
Sebastian Ullrich 2020-01-19 17:12:34 +01:00 • committed by Leonardo de Moura
parent 9790b2b390
commit 7f4e1db86b
2 changed files with 8 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Lean/Elab/BuiltinNotation.lean
View file

@ -24,14 +24,14 @@ adaptExpander $ fun stx => match_syntax stx with
@[builtinTermElab «if»] def elabIf : TermElab :=
adaptExpander $ fun stx => match_syntax stx with
| `(if $h : $cond then $t else $e) => let h := mkTermIdFromIdent h; `(dite $cond (fun $h => $t) (fun $h => $e))
| `(if $h : $cond then $t else $e) => `(dite $cond (fun $h:ident => $t) (fun $h:ident => $e))
| `(if $cond then $t else $e) => `(ite $cond $t $e)
| _ => throwUnsupportedSyntax
@[builtinTermElab subtype] def elabSubtype : TermElab :=
adaptExpander $ fun stx => match_syntax stx with
| `({ $x : $type // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : $type) => $p))
| `({ $x // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : _) => $p))
| `({ $x : $type // $p }) => `(Subtype (fun ($x:ident : $type) => $p))
| `({ $x // $p }) => `(Subtype (fun ($x:ident : _) => $p))
| _ => throwUnsupportedSyntax
@[builtinTermElab anonymousCtor] def elabAnoymousCtor : TermElab :=
@ -66,8 +66,8 @@ adaptExpander $ fun stx => match_syntax stx with
adaptExpander $ fun stx => match_syntax stx with
| `(have $type from $val; $body) => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val)
| `(have $type := $val; $body) => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val)
| `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
| `(have $x : $type := $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
| `(have $x : $type from $val; $body) => `((fun ($x:ident : $type) => $body) $val)
| `(have $x : $type := $val; $body) => `((fun ($x:ident : $type) => $body) $val)
| _ => throwUnsupportedSyntax
@[termElab «where»] def elabWhere : TermElab :=

7
src/Init/Lean/Elab/TermBinders.lean
View file

@ -187,10 +187,9 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
let binder := binders.get ⟨i, h⟩;
let processAsPattern : Unit → TermElabM (Array Syntax × Syntax) := fun _ => do {
let pattern := binder;
ident ← mkFreshAnonymousIdent binder;
(binders, newBody) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident (mkHole binder));
let major := mkTermIdFromIdent ident;
newBody ← `(match $major with | $pattern => $newBody);
major ← mkFreshAnonymousIdent binder;
(binders, newBody) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder));
newBody ← `(match $major:ident with | $pattern => $newBody);
pure (binders, newBody)
};
match binder with