Instances For
@[inline]
Instances For
Equations
Instances For
Instances For
Equations
Instances For
Equations
Equations
Instances For
Instances For
Equations
- Lean.NameSet.instEmptyCollection = { emptyCollection := Lean.NameSet.empty }
Equations
- Lean.NameSet.instInhabited = { default := Lean.NameSet.empty }
Equations
Instances For
Instances For
The union of two NameSet
s.
Equations
- s.append t = Lean.RBMap.mergeBy (fun (x : Lean.Name) (x x : Unit) => ()) s t
Instances For
Equations
- Lean.NameSet.instAppend = { append := Lean.NameSet.append }
@[reducible, inline]
Equations
Instances For
Equations
- Lean.NameSSet.instEmptyCollection = { emptyCollection := Lean.NameSSet.empty }
Equations
- Lean.NameSSet.instInhabited = { default := Lean.NameSSet.empty }
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Instances For
@[inline]
Equations
Instances For
Equations
- Lean.NameHashSet.instEmptyCollection = { emptyCollection := Lean.NameHashSet.empty }
Equations
- Lean.NameHashSet.instInhabited = { default := ∅ }
Equations
Instances For
Instances For
filter f s
returns the NameHashSet
consisting of all x
in s
where f x
returns true
.