Floating point over nullables, typed

Each lifted operator has its plain counterpart's signature with an Option around every argument and around the result, and nothing else changed. The lift is strict: none unless every argument is some.

A rounding-mode argument becomes nullable along with the rest: fpAdd? takes a Term (Option Float.RoundingMode), since nullable.lift makes every argument of the lifted operator nullable and none of them optional.

def Cvc.Typed.Term.fpIsNormal? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

• fp.fpIsNormal? = Cvc.Untyped.Term.fpIsNormal? fp

def Cvc.Typed.Term.fpIsInf? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

• fp.fpIsInf? = Cvc.Untyped.Term.fpIsInf? fp

def Cvc.Typed.Term.fpDiv? [Ω] {e s : Nat} (rm : Term (Option Float.RoundingMode)) (lft rgt : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• rm.fpDiv? lft rgt = Cvc.Untyped.Term.fpDiv? rm lft rgt

def Cvc.Typed.Term.fpGe? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.fpRti? [Ω] {e s : Nat} (rm : Term (Option Float.RoundingMode)) (fp : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• rm.fpRti? fp = Cvc.Untyped.Term.fpRti? rm fp

def Cvc.Typed.Term.fpRem? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

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

def Cvc.Typed.Term.fpEq? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.fpSub? [Ω] {e s : Nat} (rm : Term (Option Float.RoundingMode)) (lft rgt : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• rm.fpSub? lft rgt = Cvc.Untyped.Term.fpSub? rm lft rgt

def Cvc.Typed.Term.fpAdd? [Ω] {e s : Nat} (rm : Term (Option Float.RoundingMode)) (lft rgt : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• rm.fpAdd? lft rgt = Cvc.Untyped.Term.fpAdd? rm lft rgt

def Cvc.Typed.Term.fpToReal? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Rat))

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

Equations

• fp.fpToReal? = Cvc.Untyped.Term.fpToReal? fp

def Cvc.Typed.Term.fpSqrt? [Ω] {e s : Nat} (rm : Term (Option Float.RoundingMode)) (fp : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• rm.fpSqrt? fp = Cvc.Untyped.Term.fpSqrt? rm fp

def Cvc.Typed.Term.fpIsNan? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

• fp.fpIsNan? = Cvc.Untyped.Term.fpIsNan? fp

def Cvc.Typed.Term.fpNeg? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• fp.fpNeg? = Cvc.Untyped.Term.fpNeg? fp

def Cvc.Typed.Term.fpIsSubnormal? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

• fp.fpIsSubnormal? = Cvc.Untyped.Term.fpIsSubnormal? fp

def Cvc.Typed.Term.fpIsPos? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

• fp.fpIsPos? = Cvc.Untyped.Term.fpIsPos? fp

def Cvc.Typed.Term.fpIsZero? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

• fp.fpIsZero? = Cvc.Untyped.Term.fpIsZero? fp

def Cvc.Typed.Term.fpLe? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.fpMax? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

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

def Cvc.Typed.Term.fpMul? [Ω] {e s : Nat} (rm : Term (Option Float.RoundingMode)) (lft rgt : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• rm.fpMul? lft rgt = Cvc.Untyped.Term.fpMul? rm lft rgt

def Cvc.Typed.Term.fpGt? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.fpLt? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

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

def Cvc.Typed.Term.fpOfBits? [Ω] {e s : Nat} (sign : Term (Option (BitVec 1))) (exponent : Term (Option (BitVec e))) (significand : Term (Option (BitVec s))) : Env (Term (Option (Float e (s + 1))))

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

Equations

• sign.fpOfBits? exponent significand = Cvc.Untyped.Term.fpOfBits? sign exponent significand

def Cvc.Typed.Term.fpMin? [Ω] {e s : Nat} (lft rgt : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

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

def Cvc.Typed.Term.fpAbs? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• fp.fpAbs? = Cvc.Untyped.Term.fpAbs? fp

def Cvc.Typed.Term.fpFma? [Ω] {e s : Nat} (rm : Term (Option Float.RoundingMode)) (a b c : Term (Option (Float e s))) : Env (Term (Option (Float e s)))

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

Equations

• rm.fpFma? a b c = Cvc.Untyped.Term.fpFma? rm a b c

def Cvc.Typed.Term.fpIsNeg? [Ω] {e s : Nat} (fp : Term (Option (Float e s))) : Env (Term (Option Bool))

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

Equations

• fp.fpIsNeg? = Cvc.Untyped.Term.fpIsNeg? fp