Bags over nullables, sort-erased

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

The bag term becomes nullable, not its elements: (Nullable (Bag T)), not (Bag (Nullable T)).

def Cvc.Untyped.Term.bagAll? [Ω] (p b : Term) : Env Term

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

Equations

• p.bagAll? b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_ALL #[p, b]

def Cvc.Untyped.Term.bagFold? [Ω] (f init b : Term) : Env Term

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

Equations

• f.bagFold? init b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_FOLD #[f, init, b]

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

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

Equations

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

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

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

Equations

• elm.bagCount? b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_COUNT #[elm, b]

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

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

Equations

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

def Cvc.Untyped.Term.bagMap? [Ω] (f b : Term) : Env Term

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

Equations

• f.bagMap? b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_MAP #[f, b]

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

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

Equations

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

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

bagUnionDisjoint? over two or more terms.

Equations

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

def Cvc.Untyped.Term.bagCard? [Ω] (b : Term) : Env Term

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

Equations

• b.bagCard? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_CARD #[b]

def Cvc.Untyped.Term.bagFilter? [Ω] (p b : Term) : Env Term

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

Equations

• p.bagFilter? b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_FILTER #[p, b]

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

bagUnionMax? over two or more terms.

Equations

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

def Cvc.Untyped.Term.bagSome? [Ω] (p b : Term) : Env Term

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

Equations

• p.bagSome? b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_SOME #[p, b]

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

bagInterMin? over two or more terms.

Equations

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

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

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

Equations

• elm.bagMember? b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_MEMBER #[elm, b]

def Cvc.Untyped.Term.bagSetof? [Ω] (b : Term) : Env Term

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

Equations

• b.bagSetof? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_SETOF #[b]

def Cvc.Untyped.Term.bagPartition? [Ω] (p b : Term) : Env Term

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

Equations

• p.bagPartition? b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_PARTITION #[p, b]

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

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

Equations

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

def Cvc.Untyped.Term.bagChoose? [Ω] (b : Term) : Env Term

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

Equations

• b.bagChoose? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_CHOOSE #[b]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• elm.bagMake? count = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.BAG_MAKE #[elm, count]