Generated arithmetic constructors, sort-erased

def Cvc.Untyped.Term.smtOp.nary.ge : Lean.ParserDescr

Equations

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

def Cvc.Untyped.Term.smtOp.nary.lt : Lean.ParserDescr

Equations

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

def Cvc.Untyped.Term.smtOp.nary.gt : Lean.ParserDescr

Equations

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

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

Euclidean integer division, left-associative; unspecified on a zero divisor.

Equations

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

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

Base-two logarithm.

Equations

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

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

Arithmetic negation.

Equations

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

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.mkTerm cvc5.Kind.SUB terms

def Cvc.Untyped.Term.mkReal [Ω] (r : Rat) : Env Term

A real literal.

Equations

• Cvc.Untyped.Term.mkReal r = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkRealOfRat r

def Cvc.Untyped.Term.mkIntOfString [Ω] (repr : String) : Env Term

An integer literal, read from its decimal representation.

Equations

• Cvc.Untyped.Term.mkIntOfString repr = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkIntegerOfString repr

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

Binary greater-than; gtN chains, as ltN does.

Equations

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

def Cvc.Untyped.Term.smtOp.nary.mul : Lean.ParserDescr

Equations

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

def Cvc.Untyped.Term.pi [Ω] : Env Term

The constant π.

Equations

• Cvc.Untyped.Term.pi = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkPi

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

mul over any number of terms: none gives 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.le [Ω] (lft rgt : Term) : Env Term

Binary less-than-or-equal-to; leN chains, as ltN does.

Equations

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

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

Cosecant.

Equations

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

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

Two raised to a non-negative exponent.

Equations

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

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

Conversion to an integer, rounding towards negative infinity.

Equations

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

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.mkTerm cvc5.Kind.GEQ terms

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

Real division, left-associative; unspecified on a zero divisor.

Equations

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

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.mkTerm cvc5.Kind.INTS_DIVISION_TOTAL terms

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

Bit-wise and of the low size bits of lft and rgt; zero when size ≤ 0.

Equations

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

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

Euclidean integer division, left-associative; zero on a zero divisor.

Equations

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

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

Absolute value.

Equations

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

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

Arc cotangent.

Equations

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

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.mkTerm cvc5.Kind.LT terms

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

Exponentiation.

Equations

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

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

Arc tangent.

Equations

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

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

Arc cosecant.

Equations

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

def Cvc.Untyped.Term.smtOp.binary.ge : Lean.TrailingParserDescr

Equations

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

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.mkTerm cvc5.Kind.LEQ terms

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

Binary subtraction; subN is left-associative.

Equations

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

def Cvc.Untyped.Term.divisible [Ω] (divisor : Nat) (arg : Term) : Env Term

Whether arg is divisible by divisor.

Equations

• Cvc.Untyped.Term.divisible divisor arg = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => do let __do_lift ← tm.mkOpOfIndices cvc5.Kind.DIVISIBLE #[divisor] tm.mkTermOfOp __do_lift #[arg]

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

Cosine.

Equations

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

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

Euclidean integer modulus; the dividend on a zero divisor.

Equations

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

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.mkTerm cvc5.Kind.DIVISION terms

def Cvc.Untyped.Term.smtOp.binary.lt : Lean.TrailingParserDescr

Equations

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

def Cvc.Untyped.Term.smtOp.binary.gt : Lean.TrailingParserDescr

Equations

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

def Cvc.Untyped.Term.smtOp.nary.add : Lean.ParserDescr

Equations

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

def Cvc.Untyped.Term.smtOp.binary.intMod : Lean.TrailingParserDescr

Equations

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

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

Binary addition.

Equations

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

def Cvc.Untyped.Term.smtOp.prefix.neg : Lean.ParserDescr

Equations

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

def Cvc.Untyped.Term.mkRealOfString [Ω] (repr : String) : Env Term

A real literal, read from a decimal ("1.5") or a fraction ("3/4").

Equations

• Cvc.Untyped.Term.mkRealOfString repr = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkRealOfString repr

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

Cotangent.

Equations

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

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

Arc secant.

Equations

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

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

Binary multiplication.

Equations

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

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

Binary greater-than-or-equal-to; geN chains, as ltN does.

Equations

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

def Cvc.Untyped.Term.smtOp.nary.le : Lean.ParserDescr

Equations

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

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

add over any number of terms: none gives 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.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.mkTerm cvc5.Kind.MULT terms

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.mkTerm cvc5.Kind.GT terms

def Cvc.Untyped.Term.smtOp.binary.sub : Lean.TrailingParserDescr

Equations

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

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

Square root.

Equations

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

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

Conversion to a real.

Equations

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

def Cvc.Untyped.Term.smtOp.binary.add : Lean.TrailingParserDescr

Equations

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

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

Whether an arithmetic term denotes an integer.

Equations

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

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

Sine.

Equations

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

def Cvc.Untyped.Term.iand [Ω] (size : Nat) (lft rgt : Term) : Env Term

Bit-wise and of the low size bits of lft and rgt.

Equations

• Cvc.Untyped.Term.iand size lft rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => do let __do_lift ← tm.mkOpOfIndices cvc5.Kind.IAND #[size] tm.mkTermOfOp __do_lift #[lft, rgt]

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

Tangent.

Equations

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

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

The exponential function.

Equations

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

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.mkTerm cvc5.Kind.INTS_DIVISION terms

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

Real division, left-associative; zero on a zero divisor.

Equations

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

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

Secant.

Equations

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

def Cvc.Untyped.Term.smtOp.binary.le : Lean.TrailingParserDescr

Equations

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

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.mkTerm cvc5.Kind.DIVISION_TOTAL terms

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

Binary less-than; ltN chains: ltN #[a, b, c] is a < b ∧ b < c.

Equations

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

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

Euclidean integer modulus, never negative; unspecified on a zero divisor.

Equations

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

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

Arc sine.

Equations

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

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

Arc cosine.

Equations

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

def Cvc.Untyped.Term.mkInt [Ω] (i : Int) : Env Term

An integer literal.

Equations

• Cvc.Untyped.Term.mkInt i = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkInteger i

def Cvc.Untyped.Term.smtOp.binary.mul : Lean.TrailingParserDescr

Equations

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

def Cvc.Untyped.Term.smtOp.nary.sub : Lean.ParserDescr

Equations

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

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.mkTerm cvc5.Kind.ADD terms

def Cvc.Untyped.View.Arith.of? [Ω] (viewed : Term) : Option View.Arith

Takes a term apart one level, if Arith owns its operator.

Equations

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

inductive Cvc.Untyped.View.Arith [Ω] : Type

Arith's operators, taken apart one level, sort-erased.

• neg [Ω] (arithTerm : Term) : View.Arith

  Arithmetic negation.

• add [Ω] (kids : Kids) : View.Arith

  Binary addition.

  kids holds every operand, two or more.

• sub [Ω] (kids : Kids) : View.Arith

  Binary subtraction; subN is left-associative.

  kids holds every operand, two or more.

• mul [Ω] (kids : Kids) : View.Arith

  Binary multiplication.

  kids holds every operand, two or more.

• abs [Ω] (arithTerm : Term) : View.Arith

  Absolute value.

• lt [Ω] (kids : Kids) : View.Arith

  Binary less-than; ltN chains: ltN #[a, b, c] is a < b ∧ b < c.

  kids holds every operand, two or more.

• le [Ω] (kids : Kids) : View.Arith

  Binary less-than-or-equal-to; leN chains, as ltN does.

  kids holds every operand, two or more.

• gt [Ω] (kids : Kids) : View.Arith

  Binary greater-than; gtN chains, as ltN does.

  kids holds every operand, two or more.

• ge [Ω] (kids : Kids) : View.Arith

  Binary greater-than-or-equal-to; geN chains, as ltN does.

  kids holds every operand, two or more.

• isInt [Ω] (arithTerm : Term) : View.Arith

  Whether an arithmetic term denotes an integer.

• realDiv [Ω] (kids : Kids) : View.Arith

  Real division, left-associative; unspecified on a zero divisor.

  kids holds every operand, two or more.

• realDivTotal [Ω] (kids : Kids) : View.Arith

  Real division, left-associative; zero on a zero divisor.

  kids holds every operand, two or more.

• intDiv [Ω] (kids : Kids) : View.Arith

  Euclidean integer division, left-associative; unspecified on a zero divisor.

  kids holds every operand, two or more.

• intDivTotal [Ω] (kids : Kids) : View.Arith

  Euclidean integer division, left-associative; zero on a zero divisor.

  kids holds every operand, two or more.

• intMod [Ω] (lft rgt : Term) : View.Arith

  Euclidean integer modulus, never negative; unspecified on a zero divisor.

• intModTotal [Ω] (lft rgt : Term) : View.Arith

  Euclidean integer modulus; the dividend on a zero divisor.

• pow [Ω] (base exponent : Term) : View.Arith

  Exponentiation.

• pow2 [Ω] (exponent : Term) : View.Arith

  Two raised to a non-negative exponent.

• log2 [Ω] (arg : Term) : View.Arith

  Base-two logarithm.

• sqrt [Ω] (arg : Term) : View.Arith

  Square root.

• exp [Ω] (arg : Term) : View.Arith

  The exponential function.

• toReal [Ω] (arithTerm : Term) : View.Arith

  Conversion to a real.

• toInt [Ω] (arithTerm : Term) : View.Arith

  Conversion to an integer, rounding towards negative infinity.

• piand [Ω] (size lft rgt : Term) : View.Arith

  Bit-wise and of the low size bits of lft and rgt; zero when size ≤ 0.

• sine [Ω] (arg : Term) : View.Arith

  Sine.

• cosine [Ω] (arg : Term) : View.Arith

  Cosine.

• tangent [Ω] (arg : Term) : View.Arith

  Tangent.

• cosecant [Ω] (arg : Term) : View.Arith

  Cosecant.

• secant [Ω] (arg : Term) : View.Arith

  Secant.

• cotangent [Ω] (arg : Term) : View.Arith

  Cotangent.

• arcsine [Ω] (arg : Term) : View.Arith

  Arc sine.

• arccosine [Ω] (arg : Term) : View.Arith

  Arc cosine.

• arctangent [Ω] (arg : Term) : View.Arith

  Arc tangent.

• arccosecant [Ω] (arg : Term) : View.Arith

  Arc cosecant.

• arcsecant [Ω] (arg : Term) : View.Arith

  Arc secant.

• arccotangent [Ω] (arg : Term) : View.Arith

  Arc cotangent.

• divisible [Ω] (divisor : Nat) (arg : Term) : View.Arith

  Whether arg is divisible by divisor.

• iand [Ω] (size : Nat) (lft rgt : Term) : View.Arith

  Bit-wise and of the low size bits of lft and rgt.

• pi [Ω] : View.Arith

  The constant π.

Values

Nat goes to a term but not back: the sort is Int, so reading one back would have to fail on a negative value rather than answer.

def Cvc.Untyped.Term.getSign [Ω] (term : Term) : Res Int

The sign of an integer or real value, -1, 0 or 1, failing on any other term.

Equations

• term.getSign = Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Untyped.Term.toUnsafe✝ term).getRealOrIntegerValueSign

Machine-width views

An SMT integer is unbounded, so these say whether a value happens to fit a machine word and hand it over if it does. They are views of getIntValue, not a different value.

def Cvc.Untyped.Term.isInt32Value [Ω] (term : Term) : Bool

Determine if this term is an Int32 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isInt32Value = (Cvc.Untyped.Term.toUnsafe✝ term).isInt32Value

def Cvc.Untyped.Term.getInt32Value [Ω] (term : Term) : Res Int32

Get the Int32 representation of this integral value.

NB: requires that this term is an Int32 value (see isInt32Value).

Equations

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

def Cvc.Untyped.Term.isInt64Value [Ω] (term : Term) : Bool

Determine if this term is an Int64 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isInt64Value = (Cvc.Untyped.Term.toUnsafe✝ term).isInt64Value

def Cvc.Untyped.Term.getInt64Value [Ω] (term : Term) : Res Int64

Get the Int64 representation of this integral value.

NB: requires that this term is an Int64 value (see isInt64Value).

Equations

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

def Cvc.Untyped.Term.isUInt32Value [Ω] (term : Term) : Bool

Determine if this term is an UInt32 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isUInt32Value = (Cvc.Untyped.Term.toUnsafe✝ term).isUInt32Value

def Cvc.Untyped.Term.getUInt32Value [Ω] (term : Term) : Res UInt32

Get the UInt32 representation of this integral value.

NB: requires that this term is an UInt32 value (see isUInt32Value).

Equations

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

def Cvc.Untyped.Term.isUInt64Value [Ω] (term : Term) : Bool

Determine if this term is an UInt64 value.

NB: this will return true for integer constants and real constants that have integer value.

Equations

• term.isUInt64Value = (Cvc.Untyped.Term.toUnsafe✝ term).isUInt64Value

def Cvc.Untyped.Term.getUInt64Value [Ω] (term : Term) : Res UInt64

Get the UInt64 representation of this integral value.

NB: requires that this term is an UInt64 value (see isUInt64Value).

Equations

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

def Cvc.Untyped.Term.isReal32Value [Ω] (term : Term) : Bool

Whether a term denotes a real that fits a 32-bit numerator and denominator.

Equations

• term.isReal32Value = (Cvc.Untyped.Term.toUnsafe✝ term).isReal32Value

def Cvc.Untyped.Term.getReal32Value [Ω] (term : Term) : Res (Int32 × UInt32)

The numerator and denominator of a real value, at 32 bits.

Equations

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

def Cvc.Untyped.Term.isReal64Value [Ω] (term : Term) : Bool

Whether a term denotes a real that fits a 64-bit numerator and denominator.

Equations

• term.isReal64Value = (Cvc.Untyped.Term.toUnsafe✝ term).isReal64Value

def Cvc.Untyped.Term.getReal64Value [Ω] (term : Term) : Res (Int64 × UInt64)

The numerator and denominator of a real value, at 64 bits.

Equations

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

Real algebraic numbers

A real algebraic number is not a rational, so it has no getRatValue. It is described instead by a polynomial it is a root of, together with an interval isolating that root.

def Cvc.Untyped.Term.isRealAlgebraicNumber [Ω] (term : Term) : Bool

Determine if this term is a real algebraic number.

Equations

• term.isRealAlgebraicNumber = (Cvc.Untyped.Term.toUnsafe✝ term).isRealAlgebraicNumber

def Cvc.Untyped.Term.getRealAlgebraicNumberPolynomial [Ω] (term : Term) (v : BVar) : Env Term

The polynomial a real algebraic number is a root of, written in the bound variable v.

Equations

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

def Cvc.Untyped.Term.getRealAlgebraicNumberLowerBound [Ω] (term : Term) : Env Term

Get the lower bound for a real algebraic number value.

NB: asserts isRealAlgebraicNumber.

Equations

• term.getRealAlgebraicNumberLowerBound = liftM (Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Untyped.Term.toUnsafe✝ term).getRealAlgebraicNumberLowerBound)

def Cvc.Untyped.Term.getRealAlgebraicNumberUpperBound [Ω] (term : Term) : Env Term

Get the upper bound for a real algebraic number value.

NB: asserts isRealAlgebraicNumber.

Equations

• term.getRealAlgebraicNumberUpperBound = liftM (Except.mapError Cvc.Error.ofUnsafe✝ (Cvc.Untyped.Term.toUnsafe✝ term).getRealAlgebraicNumberUpperBound)

def Cvc.Untyped.Term.isIntValue [Ω] (term : Term) : Bool

Determine if this real/integer constant term is an integral value.

Equations

• term.isIntValue = (Cvc.Untyped.Term.toUnsafe✝ term).isIntegerValue

def Cvc.Untyped.Term.getIntValue [Ω] (term : Term) : Res Int

The integer a term denotes, failing if it denotes none.

Equations

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

def Cvc.Untyped.Term.getIntValue? [Ω] (term : Term) : Option Int

The integer a term denotes, failing if it denotes none.

Equations

• term.getIntValue? = (Cvc.Untyped.Term.toUnsafe✝ term).getIntegerValue?

def Cvc.Untyped.Term.isRealValue [Ω] (term : Term) : Bool

Determine if this term is a rational value.

NB: A term of kind Kind.PI is not considered to be a real value.

Equations

• term.isRealValue = (Cvc.Untyped.Term.toUnsafe✝ term).isRealValue

def Cvc.Untyped.Term.getRealValue [Ω] (term : Term) : Res String

The real a term denotes as a string, failing if it denotes none.

Equations

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

def Cvc.Untyped.Term.getRealValue? [Ω] (term : Term) : Option String

The real a term denotes as a string, failing if it denotes none.

Equations

• term.getRealValue? = (Cvc.Untyped.Term.toUnsafe✝ term).getRealValue?

def Cvc.Untyped.Term.getRatValue [Ω] (term : Term) : Res Rat

The real a term denotes as a Rat, failing if it denotes none.

An irrational model value, which nonlinear real arithmetic can produce, is no Rat: read it as a term instead, and take it apart with the getRealAlgebraicNumber… functions.

Equations

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

def Cvc.Untyped.Term.getRatValue? [Ω] (term : Term) : Option Rat

The real a term denotes as a Rat, failing if it denotes none.

An irrational model value, which nonlinear real arithmetic can produce, is no Rat: read it as a term instead, and take it apart with the getRealAlgebraicNumber… functions.

Equations

• term.getRatValue? = (Cvc.Untyped.Term.toUnsafe✝ term).getRationalValue?

@[instance_reducible]

instance Cvc.Untyped.Term.instSrtLikeInt : SrtLike Int

Equations

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

@[instance_reducible]

instance Cvc.Untyped.Term.instValueToTermNat : ValueToTerm Nat

Equations

• Cvc.Untyped.Term.instValueToTermNat = { valueToTerm := fun [Cvc.Ω] (n : Nat) => Cvc.Untyped.Term.mkInt ↑n }

@[instance_reducible]

instance Cvc.Untyped.Term.instSrtLikeRat : SrtLike Rat

Equations

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

smt! literals

Integer and real literals in smt!. Without this module smt! accepts neither.

def Cvc.Untyped.Term.smtNum : Lean.ParserDescr

Integer literal.

Equations

• Cvc.Untyped.Term.smtNum = Lean.ParserDescr.node `Cvc.Untyped.Term.smtNum 1024 (Lean.ParserDescr.const `num)

def Cvc.Untyped.Term.smtSci : Lean.ParserDescr

Real literal, 1.5 or 1.5e-3.

Equations

• Cvc.Untyped.Term.smtSci = Lean.ParserDescr.node `Cvc.Untyped.Term.smtSci 1024 (Lean.ParserDescr.const `scientific)