Documentation

Lake.Util.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
@[inline]
Equations
  • Lake.NameMap.empty = Lean.RBMap.empty
instance Lake.instForInNameMapProdName_lake {m : Type u_1 → Type u_2} {α : Type} :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Lake.instCoeRBMapNameQuickCmpNameMap_lake = { coe := id }
@[reducible, inline]
abbrev Lake.OrdNameMap (α : Type u_1) :
Type u_1
Equations
@[inline]
Equations
  • Lake.OrdNameMap.empty = Lake.RBArray.empty
@[inline]
Equations
@[reducible, inline]
abbrev Lake.DNameMap (α : Lake.NameType u_1) :
Type u_1
Equations
@[inline]
Equations
  • Lake.DNameMap.empty = Lake.DRBMap.empty
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.

Name Helpers #

@[simp]
theorem Lake.Name.beq_false (m : Lake.Name) (n : Lake.Name) :
(m == n) = false ¬m = n
@[simp]
theorem Lake.Name.isPrefixOf_self {n : Lake.Name} :
n.isPrefixOf n = true
@[simp]
theorem Lake.Name.isPrefixOf_append {n : Lake.Name} {m : Lake.Name} :
¬n.hasMacroScopes = true¬m.hasMacroScopes = truen.isPrefixOf (n ++ m) = true
@[simp]
theorem Lake.Name.quickCmpAux_iff_eq {n : Lake.Name} {n' : Lake.Name} :
n.quickCmpAux n' = Ordering.eq n = n'
theorem Lake.Name.eq_of_quickCmp {n : Lake.Name} {n' : Lake.Name} :
n.quickCmp n' = Ordering.eqn = n'
Equations