Boolean and sort-generic over nullables, sort-erased

One lifted constructor per liftable operator, <id>?, each answering 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.Untyped.Term.equalN'? [Ω] (terms : Terms) (on0 : Env Term := mkBool true >>= nullableSome) (on1 : Term → Env Term := fun (x : Term) => mkBool true >>= nullableSome) : Env Term

equal? over any number of terms: none gives some true, one gives some true. on0 and on1 override these.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

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

def Cvc.Untyped.Term.orN'? [Ω] (terms : Terms) (on0 : Env Term := mkBool false >>= nullableSome) (on1 : Term → Env Term := pure) : Env Term

or? over any number of terms: none gives some false, one gives that term. on0 and on1 override these.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

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

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

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

Equations

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

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

distinct? over two or more terms.

Equations

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

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

equal? over two or more terms.

Equations

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

def Cvc.Untyped.Term.andN'? [Ω] (terms : Terms) (on0 : Env Term := mkBool true >>= nullableSome) (on1 : Term → Env Term := pure) : Env Term

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

Equations

• One or more equations did not get rendered due to their size.

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

or? over two or more terms.

Equations

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

def Cvc.Untyped.Term.xorN'? [Ω] (terms : Terms) (on0 : Env Term := mkBool false >>= nullableSome) (on1 : Term → Env Term := pure) : Env Term

xor? over any number of terms: none gives some false, one gives that term. on0 and on1 override these.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Term.ite? [Ω] (cnd thn els : Term) : Env Term

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

Equations

• cnd.ite? thn els = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ITE #[cnd, thn, els]

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

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

Equations

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

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

and? over two or more terms.

Equations

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

def Cvc.Untyped.Term.not? [Ω] (boolTerm : Term) : Env Term

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

Equations

• boolTerm.not? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.NOT #[boolTerm]

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

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

Equations

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

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

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

Equations

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

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

xor? over two or more terms.

Equations

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

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

implies? over two or more terms.

Equations

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