Boolean and sort-generic 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.

equal? is not Option's equality. The lift is strict, so equal? of two nones is none, not some true. The same goes for distinct? and for ite?, which is strict in its condition.

def Cvc.Typed.Term.xorN'? [Ω] (terms : Terms (Option Bool)) : Env (Term (Option Bool))

xor? over any number of terms: none gives some false, one gives that term.

Equations

• Cvc.Typed.Term.xorN'? terms = Cvc.Untyped.Term.xorN'? terms

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

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

Equations

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

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

xor? over two or more terms.

Equations

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

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

equal? over two or more terms.

Equations

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

def Cvc.Typed.Term.equalN'? [Ω] {α : Type} (terms : Terms (Option α)) : Env (Term (Option Bool))

equal? over any number of terms: none gives some true, one gives some true.

Equations

• Cvc.Typed.Term.equalN'? terms = Cvc.Untyped.Term.equalN'? terms

def Cvc.Typed.Term.or? [Ω] (lft rgt : Term (Option Bool)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.orN'? [Ω] (terms : Terms (Option Bool)) : Env (Term (Option Bool))

or? over any number of terms: none gives some false, one gives that term.

Equations

• Cvc.Typed.Term.orN'? terms = Cvc.Untyped.Term.orN'? terms

def Cvc.Typed.Term.implies? [Ω] (lft rgt : Term (Option Bool)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.xor? [Ω] (lft rgt : Term (Option Bool)) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.ite? [Ω] {α : Type} (cnd : Term (Option Bool)) (thn els : Term (Option α)) : Env (Term (Option α))

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

Equations

• cnd.ite? thn els = Cvc.Untyped.Term.ite? cnd thn els

def Cvc.Typed.Term.and? [Ω] (lft rgt : Term (Option Bool)) : Env (Term (Option Bool))

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

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.not? [Ω] (boolTerm : Term (Option Bool)) : Env (Term (Option Bool))

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

Equations

• boolTerm.not? = Cvc.Untyped.Term.not? boolTerm

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

implies? over two or more terms.

Equations

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

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

distinct? over two or more terms.

Equations

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

def Cvc.Typed.Term.andN'? [Ω] (terms : Terms (Option Bool)) : Env (Term (Option Bool))

and? over any number of terms: none gives some true, one gives that term.

Equations

• Cvc.Typed.Term.andN'? terms = Cvc.Untyped.Term.andN'? terms

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

and? over two or more terms.

Equations

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

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

or? over two or more terms.

Equations

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