Arithmetic over nullables, typed

Each lifted operator has its plain counterpart's signature with an Option around every argument and around the result, so add? : Term (Option α) → Term (Option α) → Env (Term (Option α)) under the same IsArith α. Everything the plain operator checks is checked here.

The lift is strict: none unless every argument is some.

def Cvc.Typed.Term.cotangent? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.cotangent? = Cvc.Untyped.Term.cotangent? arg

def Cvc.Typed.Term.geN? [Ω] {α : Type} [ToTyp α] [IsArith α] (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))

ge? over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.toReal? [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term (Option α)) : Env (Term (Option Rat))

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

Equations

• arithTerm.toReal? = Cvc.Untyped.Term.toReal? arithTerm

def Cvc.Typed.Term.mulN? [Ω] {α : Type} [ToTyp α] [IsArith α] (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 α))

mul? over two or more terms.

Equations

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

def Cvc.Typed.Term.arccotangent? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.arccotangent? = Cvc.Untyped.Term.arccotangent? arg

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

mul? over any number of terms: none gives some 1, one gives that term.

Equations

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

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

intDivTotal? over two or more terms.

Equations

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

def Cvc.Typed.Term.abs? [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term (Option α)) : Env (Term (Option α))

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

Equations

• arithTerm.abs? = Cvc.Untyped.Term.abs? arithTerm

def Cvc.Typed.Term.log2? [Ω] (arg : Term (Option Int)) : Env (Term (Option Int))

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

Equations

• arg.log2? = Cvc.Untyped.Term.log2? arg

def Cvc.Typed.Term.arcsecant? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.arcsecant? = Cvc.Untyped.Term.arcsecant? arg

def Cvc.Typed.Term.arccosecant? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.arccosecant? = Cvc.Untyped.Term.arccosecant? arg

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

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

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.pow? [Ω] {α : Type} [ToTyp α] [IsArith α] (base exponent : Term (Option α)) : Env (Term (Option α))

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

Equations

• base.pow? exponent = Cvc.Untyped.Term.pow? base exponent

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

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

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.gtN? [Ω] {α : Type} [ToTyp α] [IsArith α] (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))

gt? over two or more terms.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

intDiv? over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.sine? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.sine? = Cvc.Untyped.Term.sine? arg

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

realDivTotal? over two or more terms.

Equations

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

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

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

Equations

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

def Cvc.Typed.Term.ltN? [Ω] {α : Type} [ToTyp α] [IsArith α] (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))

lt? over two or more terms.

Equations

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

def Cvc.Typed.Term.sqrt? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.sqrt? = Cvc.Untyped.Term.sqrt? arg

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

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

Equations

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

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

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

Equations

• size.piand? lft rgt = Cvc.Untyped.Term.piand? size lft rgt

def Cvc.Typed.Term.arcsine? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.arcsine? = Cvc.Untyped.Term.arcsine? arg

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

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

Equations

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

def Cvc.Typed.Term.exp? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.exp? = Cvc.Untyped.Term.exp? arg

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

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

Equations

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

def Cvc.Typed.Term.neg? [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term (Option α)) : Env (Term (Option α))

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

Equations

• arithTerm.neg? = Cvc.Untyped.Term.neg? arithTerm

def Cvc.Typed.Term.cosine? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.cosine? = Cvc.Untyped.Term.cosine? arg

def Cvc.Typed.Term.subN? [Ω] {α : Type} [ToTyp α] [IsArith α] (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 α))

sub? over two or more terms.

Equations

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

def Cvc.Typed.Term.pow2? [Ω] (exponent : Term (Option Int)) : Env (Term (Option Int))

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

Equations

• exponent.pow2? = Cvc.Untyped.Term.pow2? exponent

def Cvc.Typed.Term.isInt? [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term (Option α)) : Env (Term (Option Bool))

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

Equations

• arithTerm.isInt? = Cvc.Untyped.Term.isInt? arithTerm

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

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

Equations

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

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

realDiv? over two or more terms.

Equations

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

def Cvc.Typed.Term.tangent? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.tangent? = Cvc.Untyped.Term.tangent? arg

def Cvc.Typed.Term.leN? [Ω] {α : Type} [ToTyp α] [IsArith α] (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))

le? over two or more terms.

Equations

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

def Cvc.Typed.Term.arccosine? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.arccosine? = Cvc.Untyped.Term.arccosine? arg

def Cvc.Typed.Term.toInt? [Ω] {α : Type} [ToTyp α] [IsArith α] (arithTerm : Term (Option α)) : Env (Term (Option Int))

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

Equations

• arithTerm.toInt? = Cvc.Untyped.Term.toInt? arithTerm

def Cvc.Typed.Term.arctangent? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.arctangent? = Cvc.Untyped.Term.arctangent? arg

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

add? over any number of terms: none gives some 0, one gives that term.

Equations

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

def Cvc.Typed.Term.addN? [Ω] {α : Type} [ToTyp α] [IsArith α] (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 α))

add? over two or more terms.

Equations

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

def Cvc.Typed.Term.cosecant? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.cosecant? = Cvc.Untyped.Term.cosecant? arg

def Cvc.Typed.Term.secant? [Ω] (arg : Term (Option Rat)) : Env (Term (Option Rat))

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

Equations

• arg.secant? = Cvc.Untyped.Term.secant? arg