Finite fields over nullables, sort-erased #

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

The field's size is an index on the sort, not an operator index, so every operator here lifts.

source

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

Env Term

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

Equations

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

Instances For

source

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

Env Term

ffAdd? over two or more terms.

Equations

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

Instances For

source

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

Env Term

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

Equations

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

Instances For

source

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

Env Term

ffBitsum? over two or more terms.

Equations

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

Instances For

source

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

Env Term

ffMul? over two or more terms.

Equations