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

feat(library/init/lean/localcontext): add getUnusedName

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-04 13:13:57 -07:00
parent 2a914d99dd
commit 142063fee4
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
library/init/lean/localcontext.lean
View file

@ -115,6 +115,19 @@ lctx.decls.findRev (fun decl =>
| none => none
| some decl => if decl.userName == userName then some decl else none)
def usesUserName (lctx : LocalContext) (userName : Name) : Bool :=
(lctx.findFromUserName userName).isSome
partial def getUnusedNameAux (lctx : LocalContext) (suggestion : Name) : Nat → Name × Nat
| i :=
let curr := suggestion.appendIndexAfter i;
if lctx.usesUserName curr then getUnusedNameAux (i + 1)
else (curr, i + 1)
def getUnusedName (lctx : LocalContext) (suggestion : Name) : Name :=
if lctx.usesUserName suggestion then (lctx.getUnusedNameAux suggestion 1).1
else suggestion
def lastDecl (lctx : LocalContext) : Option LocalDecl :=
lctx.decls.get (lctx.decls.size - 1)