@[inline]

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

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

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

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

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]