def Lake.stringToLegalOrSimpleName (s : String) : Lean.Name

First tries to convert a string into a legal name. If that fails, defaults to making it a simple name (e.g., Lean.Name.mkSimple).

@[inline]

def Lake.NameMap.empty {α : Type} : Lean.NameMap α

instance Lake.instForInNameMapProdName_lake {m : Type u_1 → Type u_2} {α : Type} : ForIn m (Lean.NameMap α) (Lean.Name × α)

instance Lake.instCoeRBMapNameQuickCmpNameMap_lake {α : Type} : Coe (Lean.RBMap Lean.Name α Lean.Name.quickCmp) (Lean.NameMap α)

@[reducible, inline]

abbrev Lake.OrdNameMap (α : Type u_1) : Type u_1

@[inline]

def Lake.OrdNameMap.empty {α : Type u_1} : OrdNameMap α

@[inline]

def Lake.mkOrdNameMap (α : Type) : OrdNameMap α

@[reducible, inline]

abbrev Lake.DNameMap (α : Lean.Name → Type u_1) : Type u_1

@[inline]

def Lake.DNameMap.empty {α : Lean.Name → Type u_1} : DNameMap α

Name Helpers

def Lake.Name.eraseHead : Lean.Name → Lean.Name

theorem Lake.Name.eq_anonymous_of_isAnonymous {n : Lean.Name} (h : n.isAnonymous = true) : n = Lean.Name.anonymous

@[simp]

theorem Lake.Name.beq_false (m n : Lean.Name) : (m == n) = false ↔ ¬m = n

@[simp]

theorem Lake.Name.isPrefixOf_self {n : Lean.Name} : n.isPrefixOf n = true

@[simp]

theorem Lake.Name.isPrefixOf_append {n m : Lean.Name} : ¬n.hasMacroScopes = true → ¬m.hasMacroScopes = true → n.isPrefixOf (n ++ m) = true

@[simp]

theorem Lake.Name.quickCmpAux_iff_eq {n n' : Lean.Name} : n.quickCmpAux n' = Ordering.eq ↔ n = n'

instance Lake.Name.instLawfulCmpEqNameQuickCmpAux : LawfulCmpEq Lean.Name Lean.Name.quickCmpAux

theorem Lake.Name.eq_of_quickCmp {n n' : Lean.Name} : n.quickCmp n' = Ordering.eq → n = n'

theorem Lake.Name.quickCmp_rfl {n : Lean.Name} : n.quickCmp n = Ordering.eq

instance Lake.Name.instLawfulCmpEqNameQuickCmp : LawfulCmpEq Lean.Name Lean.Name.quickCmp

def Lake.Name.quoteFrom (ref : Lean.Syntax) (n : Lean.Name) (canonical : Bool := false) : Lean.Term