@[inline]

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

Equations

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

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

Equations

• Lake.instForInNameMapProdName = { forIn := fun {β} [Monad m] self init f => Lean.RBMap.forIn self init f }

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

Equations

• Lake.instCoeRBMapNameQuickCmpNameMap = { coe := id }

@[inline, reducible]

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

Equations

• Lake.OrdNameMap α = Lake.RBArray Lake.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

@[inline, reducible]

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

Equations

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

@[inline]

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

Equations

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

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} : Lean.Name.isPrefixOf n n = true

@[simp]

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

@[simp]

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

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

Equations

• Lake.Name.instLawfulCmpEqNameQuickCmpAux = Lake.LawfulCmpEq.mk @Lake.Name.instLawfulCmpEqNameQuickCmpAux.proof_2

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

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

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

Equations

• Lake.Name.instLawfulCmpEqNameQuickCmp = Lake.LawfulCmpEq.mk (_ : ∀ {a : Lake.Name}, Lean.Name.quickCmp a a = Ordering.eq)

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

Equations

• Lake.Name.quoteFrom ref Lean.Name.anonymous = { raw := (Lean.mkCIdentFrom ref `Lean.Name.anonymous).raw }
• Lake.Name.quoteFrom ref (Lean.Name.str p s) = Lean.Syntax.mkApp { raw := (Lean.mkCIdentFrom ref `Lean.Name.mkStr).raw } #[Lake.Name.quoteFrom ref p, Lean.quote `term s]
• Lake.Name.quoteFrom ref (Lean.Name.num p v) = Lean.Syntax.mkApp { raw := (Lean.mkCIdentFrom ref `Lean.Name.mkNum).raw } #[Lake.Name.quoteFrom ref p, Lean.quote `term v]