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

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-18 11:37:51 -07:00
parent fbbc77ceb6
commit 22dc784c3e
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Elab/Term.lean
View file

@ -426,9 +426,7 @@ pure e
Auxiliary method for creating fresh binder names.
Do not confuse with the method for creating fresh free/meta variable ids. -/
def mkFreshUserName : TermElabM Name :=
withFreshMacroScope do
x ← `(x);
pure x.getId
withFreshMacroScope $ MonadQuotation.addMacroScope `x
/--
Auxiliary method for creating a `Syntax.ident` containing
@ -441,9 +439,7 @@ pure $ mkIdentFrom ref n
/--
Auxiliary method for creating binder names for local instances. -/
def mkFreshInstanceName : TermElabM Name :=
withFreshMacroScope do
inst ← `(inst);
pure inst.getId
withFreshMacroScope $ MonadQuotation.addMacroScope `inst
private partial def hasCDot : Syntax → Bool
| Syntax.node k args =>