Sets

The Lean type denoting an SMT set. It is a Std.TreeSet, so its element type must be ordered — which is why the set operators take an Ord instance on it.

Converting a set to a term and back is done by Cvc.Untyped.Theory.Set and Cvc.Typed.Theory.Set.

@[reducible, inline]

abbrev Cvc.Set (α : Type) [Ord α] : Type

An SMT set: a Std.TreeSet, so its elements must be ordered.

Equations

• Cvc.Set α = Std.TreeSet α compare

def Cvc.Set.empty {α : Type} [Ord α] : Set α

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Cvc.Set.empty = Std.TreeSet.empty

def Cvc.Set.ofArray {α : Type u_1} [Ord α] (a : Array α) : Std.TreeSet α compare

Transforms an array into a tree set.

Equations

• Cvc.Set.ofArray a = Std.TreeSet.ofArray a compare

@[instance_reducible]

instance Cvc.Set.instToTyp {α : Type} [Ord α] [A : ToTyp α] : ToTyp (Set α)

Equations

• Cvc.Set.instToTyp = { typ := Cvc.Typ.set (Cvc.Typ?.typ (Cvc.ToTyp.typ α)) }

def Cvc.Set.toString {α : Type} [Ord α] [ToString α] (set : Set α) : String

String representation.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Set.instToString {α : Type} [Ord α] [ToString α] : ToString (Set α)

Equations

• Cvc.Set.instToString = { toString := Cvc.Set.toString }

def Cvc.Set.compare {α : Type} [Ord α] (s1 s2 : Set α) : Ordering

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Cvc.Set.instOrd {α : Type} [Ord α] : Ord (Set α)

Equations

• Cvc.Set.instOrd = { compare := Cvc.Set.compare }