Bags 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 bag term becomes nullable, not its elements — Option (Bag α), not Bag (Option α). The element type is untouched, so the Ord binders are the plain operators'.

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

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

Equations

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

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

bagInterMin? over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.bagChoose? [Ω] {α : Type} [Ord α] (b : Term (Option (Bag α))) : Env (Term (Option α))

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

Equations

• b.bagChoose? = Cvc.Untyped.Term.bagChoose? b

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

bagUnionMax? over two or more terms.

Equations

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

def Cvc.Typed.Term.bagPartition? [Ω] {α : Type} [Ord α] (p : Term (Option (α → α → Bool))) (b : Term (Option (Bag α))) : Env (Term (Option (Bag (Bag α))))

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

Equations

• p.bagPartition? b = Cvc.Untyped.Term.bagPartition? p b

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

bagUnionDisjoint? over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.bagFilter? [Ω] {α : Type} [Ord α] (p : Term (Option (α → Bool))) (b : Term (Option (Bag α))) : Env (Term (Option (Bag α)))

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

Equations

• p.bagFilter? b = Cvc.Untyped.Term.bagFilter? p b

def Cvc.Typed.Term.bagMap? [Ω] {α β : Type} [Ord α] [Ord β] (f : Term (Option (α → β))) (b : Term (Option (Bag α))) : Env (Term (Option (Bag β)))

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

Equations

• f.bagMap? b = Cvc.Untyped.Term.bagMap? f b

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

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

Equations

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

def Cvc.Typed.Term.bagCard? [Ω] {α : Type} [Ord α] (b : Term (Option (Bag α))) : Env (Term (Option Int))

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

Equations

• b.bagCard? = Cvc.Untyped.Term.bagCard? b

def Cvc.Typed.Term.bagSetof? [Ω] {α : Type} [Ord α] (b : Term (Option (Bag α))) : Env (Term (Option (Bag α)))

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

Equations

• b.bagSetof? = Cvc.Untyped.Term.bagSetof? b

def Cvc.Typed.Term.bagMake? [Ω] {α : Type} [Ord α] (elm : Term (Option α)) (count : Term (Option Int)) : Env (Term (Option (Bag α)))

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

Equations

• elm.bagMake? count = Cvc.Untyped.Term.bagMake? elm count

def Cvc.Typed.Term.bagFold? [Ω] {α β : Type} [Ord α] (f : Term (Option (α → β → β))) (init : Term (Option β)) (b : Term (Option (Bag α))) : Env (Term (Option β))

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

Equations

• f.bagFold? init b = Cvc.Untyped.Term.bagFold? f init b

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

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

Equations

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

def Cvc.Typed.Term.bagAll? [Ω] {α : Type} [Ord α] (p : Term (Option (α → Bool))) (b : Term (Option (Bag α))) : Env (Term (Option Bool))

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

Equations

• p.bagAll? b = Cvc.Untyped.Term.bagAll? p b

def Cvc.Typed.Term.bagSome? [Ω] {α : Type} [Ord α] (p : Term (Option (α → Bool))) (b : Term (Option (Bag α))) : Env (Term (Option Bool))

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

Equations

• p.bagSome? b = Cvc.Untyped.Term.bagSome? p b

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

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

Equations

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

def Cvc.Typed.Term.bagMember? [Ω] {α : Type} [Ord α] (elm : Term (Option α)) (b : Term (Option (Bag α))) : Env (Term (Option Bool))

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

Equations

• elm.bagMember? b = Cvc.Untyped.Term.bagMember? elm b

def Cvc.Typed.Term.bagCount? [Ω] {α : Type} [Ord α] (elm : Term (Option α)) (b : Term (Option (Bag α))) : Env (Term (Option Int))

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

Equations

• elm.bagCount? b = Cvc.Untyped.Term.bagCount? elm b