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).

Equations

• Lake.stringToLegalOrSimpleName s = if s.toName.isAnonymous = true then Lean.Name.mkSimple s else s.toName

@[inline]

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

Equations

• Lake.NameMap.empty = Lean.RBMap.empty

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lake.instCoeRBMapNameQuickCmpNameMap_lake = { coe := id }

@[reducible, inline]

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

Equations

• Lake.OrdNameMap α = Lake.RBArray Lean.Name α Lean.Name.quickCmp

@[inline]

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

Equations

• Lake.OrdNameMap.empty = Lake.RBArray.empty

@[inline]

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

Equations

• Lake.mkOrdNameMap α = Lake.RBArray.empty

@[reducible, inline]

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

Equations

• Lake.DNameMap α = Lake.DRBMap Lean.Name α Lean.Name.quickCmp

@[inline]

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

Equations

• Lake.DNameMap.empty = Lake.DRBMap.empty

Name Helpers

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

Equations

• Lake.Name.eraseHead Lean.Name.anonymous = Lean.Name.anonymous
• Lake.Name.eraseHead (Lean.Name.anonymous.str str) = Lean.Name.anonymous
• Lake.Name.eraseHead (Lean.Name.anonymous.num i) = Lean.Name.anonymous
• Lake.Name.eraseHead (p.str s) = (Lake.Name.eraseHead p).str s
• Lake.Name.eraseHead (p.num s) = (Lake.Name.eraseHead p).num s

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

Equations

• Lake.Name.quoteFrom ref n canonical = { raw := (Lean.quote `term n).raw.copyHeadTailInfoFrom (ref.setHeadInfo (Lean.SourceInfo.fromRef ref canonical)) }