Sets over nullables, sort-erased

One lifted constructor per liftable operator, <id>?, each answering none unless every argument is some.

The set term becomes nullable, not its elements: (Nullable (Set T)), not (Set (Nullable T)).

def Cvc.Untyped.Term.setMember? [Ω] (elm s : Term) : Env Term

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

Equations

• elm.setMember? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_MEMBER #[elm, s]

def Cvc.Untyped.Term.setCard? [Ω] (s : Term) : Env Term

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

Equations

• s.setCard? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_CARD #[s]

def Cvc.Untyped.Term.setFilter? [Ω] (p s : Term) : Env Term

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

Equations

• p.setFilter? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_FILTER #[p, s]

def Cvc.Untyped.Term.setMinus? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.setMinus? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_MINUS #[lft, rgt]

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

setUnion? over two or more terms.

Equations

• Cvc.Untyped.Term.setUnionN? terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_UNION terms

def Cvc.Untyped.Term.setIsEmpty? [Ω] (s : Term) : Env Term

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

Equations

• s.setIsEmpty? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_IS_EMPTY #[s]

def Cvc.Untyped.Term.setInter? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.setInter? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_INTER #[lft, rgt]

def Cvc.Untyped.Term.setIsSingleton? [Ω] (s : Term) : Env Term

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

Equations

• s.setIsSingleton? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_IS_SINGLETON #[s]

def Cvc.Untyped.Term.setSubset? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.setSubset? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_SUBSET #[lft, rgt]

def Cvc.Untyped.Term.setComplement? [Ω] (s : Term) : Env Term

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

Equations

• s.setComplement? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_COMPLEMENT #[s]

def Cvc.Untyped.Term.setSome? [Ω] (p s : Term) : Env Term

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

Equations

• p.setSome? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_SOME #[p, s]

def Cvc.Untyped.Term.setMap? [Ω] (f s : Term) : Env Term

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

Equations

• f.setMap? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_MAP #[f, s]

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

setMinus? over two or more terms.

Equations

• Cvc.Untyped.Term.setMinusN? terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_MINUS terms

def Cvc.Untyped.Term.setSingleton? [Ω] (elm : Term) : Env Term

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

Equations

• elm.setSingleton? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_SINGLETON #[elm]

def Cvc.Untyped.Term.setUnion? [Ω] (lft rgt : Term) : Env Term

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

Equations

• lft.setUnion? rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_UNION #[lft, rgt]

def Cvc.Untyped.Term.setInsert? [Ω] (elm s : Term) : Env Term

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

Equations

• elm.setInsert? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_INSERT #[elm, s]

def Cvc.Untyped.Term.setAll? [Ω] (p s : Term) : Env Term

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

Equations

• p.setAll? s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_ALL #[p, s]

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

setInter? over two or more terms.

Equations

• Cvc.Untyped.Term.setInterN? terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_INTER terms

def Cvc.Untyped.Term.setFold? [Ω] (f init s : Term) : Env Term

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

Equations

• f.setFold? init s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_FOLD #[f, init, s]

def Cvc.Untyped.Term.setChoose? [Ω] (s : Term) : Env Term

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

Equations

• s.setChoose? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SET_CHOOSE #[s]