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} : Lake.OrdNameMap α

Equations

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

@[inline]

def Lake.mkOrdNameMap (α : Type) : Lake.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} : Lake.DNameMap α

Equations

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

instance Lake.instToJsonNameMap_lake {α : Type} [Lean.ToJson α] : Lean.ToJson (Lean.NameMap α)

Equations

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

instance Lake.instFromJsonNameMap_lake {α : Type} [Lean.FromJson α] : Lean.FromJson (Lean.NameMap α)

Equations

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

Name Helpers

@[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 : Lake.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 : Lake.LawfulCmpEq Lean.Name Lean.Name.quickCmp

def Lake.Name.quoteFrom (ref : Lean.Syntax) (n : Lean.Name) : Lean.Term

Equations

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