Sets over nullables, typed

Each lifted operator has its plain counterpart's signature with an Option around every argument and around the result, and nothing else changed. The lift is strict: none unless every argument is some.

The set term becomes nullable, not its elements — Option (Set α), not Set (Option α). The element type is untouched, so the Ord binders are the plain operators'.

def Cvc.Typed.Term.setFold? [Ω] {α β : Type} [Ord α] (f : Term (Option (α → β → β))) (init : Term (Option β)) (s : Term (Option (Set α))) : Env (Term (Option β))

setFold lifted over nullables, strictly: none unless every argument is some.

Equations

• f.setFold? init s = Cvc.Untyped.Term.setFold? f init s

def Cvc.Typed.Term.setSome? [Ω] {α : Type} [Ord α] (p : Term (Option (α → Bool))) (s : Term (Option (Set α))) : Env (Term (Option Bool))

setSome lifted over nullables, strictly: none unless every argument is some.

Equations

• p.setSome? s = Cvc.Untyped.Term.setSome? p s

def Cvc.Typed.Term.setComplement? [Ω] {α : Type} [Ord α] (s : Term (Option (Set α))) : Env (Term (Option (Set α)))

setComplement lifted over nullables, strictly: none unless every argument is some.

Equations

• s.setComplement? = Cvc.Untyped.Term.setComplement? s

def Cvc.Typed.Term.setInterN? [Ω] {α : Type} [Ord α] (terms : Terms (Option (Set α))) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Option (Set α)))

setInter? over two or more terms.

Equations

• Cvc.Typed.Term.setInterN? terms atLeastTwoElements = Cvc.Untyped.Term.setInterN? terms atLeastTwoElements

def Cvc.Typed.Term.setInter? [Ω] {α : Type} [Ord α] (lft rgt : Term (Option (Set α))) : Env (Term (Option (Set α)))

setInter lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.setInter? rgt = Cvc.Untyped.Term.setInter? lft rgt

def Cvc.Typed.Term.setIsEmpty? [Ω] {α : Type} [Ord α] (s : Term (Option (Set α))) : Env (Term (Option Bool))

setIsEmpty lifted over nullables, strictly: none unless every argument is some.

Equations

• s.setIsEmpty? = Cvc.Untyped.Term.setIsEmpty? s

def Cvc.Typed.Term.setMap? [Ω] {α β : Type} [Ord α] [Ord β] (f : Term (Option (α → β))) (s : Term (Option (Set α))) : Env (Term (Option (Set β)))

setMap lifted over nullables, strictly: none unless every argument is some.

Equations

• f.setMap? s = Cvc.Untyped.Term.setMap? f s

def Cvc.Typed.Term.setChoose? [Ω] {α : Type} [Ord α] (s : Term (Option (Set α))) : Env (Term (Option α))

setChoose lifted over nullables, strictly: none unless every argument is some.

Equations

• s.setChoose? = Cvc.Untyped.Term.setChoose? s

def Cvc.Typed.Term.setFilter? [Ω] {α : Type} [Ord α] (p : Term (Option (α → Bool))) (s : Term (Option (Set α))) : Env (Term (Option (Set α)))

setFilter lifted over nullables, strictly: none unless every argument is some.

Equations

• p.setFilter? s = Cvc.Untyped.Term.setFilter? p s

def Cvc.Typed.Term.setUnion? [Ω] {α : Type} [Ord α] (lft rgt : Term (Option (Set α))) : Env (Term (Option (Set α)))

setUnion lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.setUnion? rgt = Cvc.Untyped.Term.setUnion? lft rgt

def Cvc.Typed.Term.setAll? [Ω] {α : Type} [Ord α] (p : Term (Option (α → Bool))) (s : Term (Option (Set α))) : Env (Term (Option Bool))

setAll lifted over nullables, strictly: none unless every argument is some.

Equations

• p.setAll? s = Cvc.Untyped.Term.setAll? p s

def Cvc.Typed.Term.setUnionN? [Ω] {α : Type} [Ord α] (terms : Terms (Option (Set α))) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Option (Set α)))

setUnion? over two or more terms.

Equations

• Cvc.Typed.Term.setUnionN? terms atLeastTwoElements = Cvc.Untyped.Term.setUnionN? terms atLeastTwoElements

def Cvc.Typed.Term.setSingleton? [Ω] {α : Type} [Ord α] (elm : Term (Option α)) : Env (Term (Option (Set α)))

setSingleton lifted over nullables, strictly: none unless every argument is some.

Equations

• elm.setSingleton? = Cvc.Untyped.Term.setSingleton? elm

def Cvc.Typed.Term.setMinusN? [Ω] {α : Type} [Ord α] (terms : Terms (Option (Set α))) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term (Option (Set α)))

setMinus? over two or more terms.

Equations

• Cvc.Typed.Term.setMinusN? terms atLeastTwoElements = Cvc.Untyped.Term.setMinusN? terms atLeastTwoElements

def Cvc.Typed.Term.setSubset? [Ω] {α : Type} [Ord α] (lft rgt : Term (Option (Set α))) : Env (Term (Option Bool))

setSubset lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.setSubset? rgt = Cvc.Untyped.Term.setSubset? lft rgt

def Cvc.Typed.Term.setMinus? [Ω] {α : Type} [Ord α] (lft rgt : Term (Option (Set α))) : Env (Term (Option (Set α)))

setMinus lifted over nullables, strictly: none unless every argument is some.

Equations

• lft.setMinus? rgt = Cvc.Untyped.Term.setMinus? lft rgt

def Cvc.Typed.Term.setCard? [Ω] {α : Type} [Ord α] (s : Term (Option (Set α))) : Env (Term (Option Int))

setCard lifted over nullables, strictly: none unless every argument is some.

Equations

• s.setCard? = Cvc.Untyped.Term.setCard? s

def Cvc.Typed.Term.setInsert? [Ω] {α : Type} [Ord α] (elm : Term (Option α)) (s : Term (Option (Set α))) : Env (Term (Option (Set α)))

setInsert lifted over nullables, strictly: none unless every argument is some.

Equations

• elm.setInsert? s = Cvc.Untyped.Term.setInsert? elm s

def Cvc.Typed.Term.setIsSingleton? [Ω] {α : Type} [Ord α] (s : Term (Option (Set α))) : Env (Term (Option Bool))

setIsSingleton lifted over nullables, strictly: none unless every argument is some.

Equations

• s.setIsSingleton? = Cvc.Untyped.Term.setIsSingleton? s

def Cvc.Typed.Term.setMember? [Ω] {α : Type} [Ord α] (elm : Term (Option α)) (s : Term (Option (Set α))) : Env (Term (Option Bool))

setMember lifted over nullables, strictly: none unless every argument is some.

Equations

• elm.setMember? s = Cvc.Untyped.Term.setMember? elm s