Lean.Data.NameMap.Basic

source

def Lean.NameMap (α : Type) :

Type

Instances For

source

@[inline]

def Lean.mkNameMap (α : Type) :

NameMap α

Instances For

source

@[implicit_reducible]

instance Lean.NameMap.instRepr {α : Type} [Repr α] :

Repr (NameMap α)

source

@[implicit_reducible]

instance Lean.NameMap.instEmptyCollection (α : Type) :

EmptyCollection (NameMap α)

source

@[implicit_reducible]

instance Lean.NameMap.instInhabited (α : Type) :

Inhabited (NameMap α)

source

def Lean.NameMap.insert {α : Type} (m : NameMap α) (n : Name) (a : α) :

Std.TreeMap Name α Name.quickCmp

Instances For

source

def Lean.NameMap.contains {α : Type} (m : NameMap α) (n : Name) :

Bool

Instances For

source

def Lean.NameMap.find? {α : Type} (m : NameMap α) (n : Name) :

Option α

Instances For

source

@[implicit_reducible]

instance Lean.NameMap.instForInProdNameOfMonad {α : Type} {m : Type u_1 → Type u_2} [Monad m] :

ForIn m (NameMap α) (Name × α)

source

def Lean.NameMap.filter {α : Type} (f : Name → α → Bool) (m : NameMap α) :

NameMap α

filter f m returns the NameMap consisting of all "key/val"-pairs in m where f key val returns true.

Instances For

source

def Lean.NameSet :

Type

Instances For

source

def Lean.NameSet.empty :

NameSet

Instances For

source

@[implicit_reducible]

instance Lean.NameSet.instEmptyCollection :

EmptyCollection NameSet

source

@[implicit_reducible]

instance Lean.NameSet.instInhabited :

Inhabited NameSet

source

def Lean.NameSet.insert (s : NameSet) (n : Name) :

NameSet

Instances For

source

def Lean.NameSet.contains (s : NameSet) (n : Name) :

Bool

Instances For

source

@[implicit_reducible]

instance Lean.NameSet.instForInNameOfMonad {m : Type u_1 → Type u_2} [Monad m] :

ForIn m NameSet Name

source

def Lean.NameSet.append (s t : NameSet) :

NameSet

The union of two NameSets.

Instances For

source

@[implicit_reducible]

instance Lean.NameSet.instAppend :

Append NameSet

source

@[implicit_reducible]

instance Lean.NameSet.instSingletonName :

Singleton Name NameSet

source

@[implicit_reducible]

instance Lean.NameSet.instUnion :

Union NameSet

source

@[implicit_reducible]

instance Lean.NameSet.instInter :

Inter NameSet

source

@[implicit_reducible]

instance Lean.NameSet.instSDiff :

SDiff NameSet

source

def Lean.NameSet.filter (f : Name → Bool) (s : NameSet) :

NameSet

filter f s returns the NameSet consisting of all x in s where f x returns true.

Instances For

source

def Lean.NameSet.ofList (l : List Name) :

NameSet

Instances For

source

def Lean.NameSet.ofArray (l : Array Name) :

Instances For

def Lean.NameSSet :

Instances For

@[reducible, inline]

abbrev Lean.NameSSet.empty :

NameSSet

Instances For

source

@[implicit_reducible]

instance Lean.NameSSet.instEmptyCollection :

EmptyCollection NameSSet

source

@[implicit_reducible]

instance Lean.NameSSet.instInhabited :

Inhabited NameSSet

source

@[reducible, inline]

abbrev Lean.NameSSet.insert (s : NameSSet) (n : Name) :

NameSSet

Instances For

source

@[reducible, inline]

abbrev Lean.NameSSet.contains (s : NameSSet) (n : Name) :

Bool

Instances For

source

def Lean.NameHashSet :

Type

Instances For

source

@[inline]

def Lean.NameHashSet.empty :

NameHashSet

Instances For

source

@[implicit_reducible]

instance Lean.NameHashSet.instEmptyCollection :

EmptyCollection NameHashSet

source

@[implicit_reducible]

instance Lean.NameHashSet.instInhabited :

Inhabited NameHashSet

source

def Lean.NameHashSet.insert (s : NameHashSet) (n : Name) :

Std.HashSet Name

Instances For

source

def Lean.NameHashSet.contains (s : NameHashSet) (n : Name) :

Bool

Instances For

source

def Lean.NameHashSet.filter (f : Name → Bool) (s : NameHashSet) :

NameHashSet

filter f s returns the NameHashSet consisting of all x in s where f x returns true.

Instances For

source

def Lean.MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) :

Bool

Instances For

source

def Lean.MacroScopesView.isSuffixOf (v₁ v₂ : MacroScopesView) :

Bool

Instances For