inductive Float.Model.UnpackedFloat.Sign : Type

Inductive with two constructors negative and positive for representing sign bits in floating-point models. This is not a general-purpose sign type like mathlib's SignType, which also includes a zero case.

• negative : Sign

  Negative (-) sign.

• positive : Sign

  Positive (+) sign.

def Float.Model.UnpackedFloat.instReprSign.repr : Sign → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Float.Model.UnpackedFloat.instReprSign : Repr Sign

Equations

• Float.Model.UnpackedFloat.instReprSign = { reprPrec := Float.Model.UnpackedFloat.instReprSign.repr }

@[instance_reducible]

instance Float.Model.UnpackedFloat.instDecidableEqSign : DecidableEq Sign

Equations

• Float.Model.UnpackedFloat.instDecidableEqSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Float.Model.UnpackedFloat.Sign.instMul : Mul Sign

Equations

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

@[instance_reducible]

instance Float.Model.UnpackedFloat.Sign.instDiv : Div Sign

Equations

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

@[instance_reducible]

instance Float.Model.UnpackedFloat.Sign.instNeg : Neg Sign

Equations

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

@[instance_reducible]

instance Float.Model.UnpackedFloat.Sign.instOrd : Ord Sign

Equations

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

def Float.Model.UnpackedFloat.Sign.apply (s : Sign) (n : Int) : Int

Apply the given sign to the given integer.

Equations

• Float.Model.UnpackedFloat.Sign.negative.apply n = -n
• Float.Model.UnpackedFloat.Sign.positive.apply n = n

def Float.Model.UnpackedFloat.Sign.toBitVec : Sign → BitVec 1

Converts the sign to a bitvector, with positive sign denoted by 0.

Equations

• Float.Model.UnpackedFloat.Sign.negative.toBitVec = 1#1
• Float.Model.UnpackedFloat.Sign.positive.toBitVec = 0#1

def Float.Model.UnpackedFloat.Sign.ofBitVec (b : BitVec 1) : Sign

Constructs a sign from a bitvector, with positive sign denoted by 0.

Equations

• Float.Model.UnpackedFloat.Sign.ofBitVec b = if b = 0#1 then Float.Model.UnpackedFloat.Sign.positive else Float.Model.UnpackedFloat.Sign.negative