From 142063fee4cc495ce48c81a3fe4e1ff5530e4fad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Aug 2019 13:13:57 -0700 Subject: [PATCH] feat(library/init/lean/localcontext): add `getUnusedName` --- library/init/lean/localcontext.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/library/init/lean/localcontext.lean b/library/init/lean/localcontext.lean index 11e01970fc..6bba0c1b9a 100644 --- a/library/init/lean/localcontext.lean +++ b/library/init/lean/localcontext.lean @@ -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)