Arithmetic over nullables, sort-erased

One lifted constructor per liftable arithmetic operator, <id>?. Each answers none unless every argument is some.

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

gt? over two or more terms.

Equations

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

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

mul? over two or more terms.

Equations

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

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

realDivTotal? over two or more terms.

Equations

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

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

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

Equations

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

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

ge? over two or more terms.

Equations

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

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

lt? over two or more terms.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

intDiv? over two or more terms.

Equations

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

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

realDiv? over two or more terms.

Equations

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

def Cvc.Untyped.Term.arcsine? [Ω] (arg : Term) : Env Term

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

Equations

• arg.arcsine? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ARCSINE #[arg]

def Cvc.Untyped.Term.toReal? [Ω] (arithTerm : Term) : Env Term

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

Equations

• arithTerm.toReal? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.TO_REAL #[arithTerm]

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

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

Equations

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

def Cvc.Untyped.Term.sqrt? [Ω] (arg : Term) : Env Term

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

Equations

• arg.sqrt? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SQRT #[arg]

def Cvc.Untyped.Term.arccotangent? [Ω] (arg : Term) : Env Term

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

Equations

• arg.arccotangent? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ARCCOTANGENT #[arg]

def Cvc.Untyped.Term.arccosecant? [Ω] (arg : Term) : Env Term

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

Equations

• arg.arccosecant? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ARCCOSECANT #[arg]

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

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

Equations

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

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

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

Equations

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

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

sub? over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Untyped.Term.sine? [Ω] (arg : Term) : Env Term

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

Equations

• arg.sine? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SINE #[arg]

def Cvc.Untyped.Term.arccosine? [Ω] (arg : Term) : Env Term

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

Equations

• arg.arccosine? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ARCCOSINE #[arg]

def Cvc.Untyped.Term.secant? [Ω] (arg : Term) : Env Term

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

Equations

• arg.secant? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.SECANT #[arg]

def Cvc.Untyped.Term.pow? [Ω] (base exponent : Term) : Env Term

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

Equations

• base.pow? exponent = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.POW #[base, exponent]

def Cvc.Untyped.Term.exp? [Ω] (arg : Term) : Env Term

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

Equations

• arg.exp? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.EXPONENTIAL #[arg]

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

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

Equations

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

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

add? over two or more terms.

Equations

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

def Cvc.Untyped.Term.arctangent? [Ω] (arg : Term) : Env Term

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

Equations

• arg.arctangent? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ARCTANGENT #[arg]

def Cvc.Untyped.Term.cosine? [Ω] (arg : Term) : Env Term

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

Equations

• arg.cosine? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.COSINE #[arg]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Cvc.Untyped.Term.neg? [Ω] (arithTerm : Term) : Env Term

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

Equations

• arithTerm.neg? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.NEG #[arithTerm]

def Cvc.Untyped.Term.cosecant? [Ω] (arg : Term) : Env Term

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

Equations

• arg.cosecant? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.COSECANT #[arg]

def Cvc.Untyped.Term.toInt? [Ω] (arithTerm : Term) : Env Term

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

Equations

• arithTerm.toInt? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.TO_INTEGER #[arithTerm]

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

le? over two or more terms.

Equations

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

def Cvc.Untyped.Term.abs? [Ω] (arithTerm : Term) : Env Term

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

Equations

• arithTerm.abs? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ABS #[arithTerm]

def Cvc.Untyped.Term.addN'? [Ω] (terms : Terms) (on0 : Env Term := mkInt 0 >>= nullableSome) (on1 : Term → Env Term := pure) : Env Term

add? over any number of terms: none gives some 0, 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.tangent? [Ω] (arg : Term) : Env Term

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

Equations

• arg.tangent? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.TANGENT #[arg]

def Cvc.Untyped.Term.arcsecant? [Ω] (arg : Term) : Env Term

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

Equations

• arg.arcsecant? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.ARCSECANT #[arg]

def Cvc.Untyped.Term.isInt? [Ω] (arithTerm : Term) : Env Term

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

Equations

• arithTerm.isInt? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.IS_INTEGER #[arithTerm]

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

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

Equations

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

def Cvc.Untyped.Term.mulN'? [Ω] (terms : Terms) (on0 : Env Term := mkInt 1 >>= nullableSome) (on1 : Term → Env Term := pure) : Env Term

mul? over any number of terms: none gives some 1, 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.cotangent? [Ω] (arg : Term) : Env Term

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

Equations

• arg.cotangent? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.COTANGENT #[arg]

def Cvc.Untyped.Term.pow2? [Ω] (exponent : Term) : Env Term

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

Equations

• exponent.pow2? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.POW2 #[exponent]

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

intDivTotal? over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Untyped.Term.log2? [Ω] (arg : Term) : Env Term

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

Equations

• arg.log2? = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkNullableLift cvc5.Kind.LOG2 #[arg]

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

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

Equations

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