Documentation

Init.Data.Float.Model.Unpacked.Sign

source
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.

Instances For
    source
    def Float.Model.UnpackedFloat.instReprSign.repr :
    Sign → Nat → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance Float.Model.UnpackedFloat.instReprSign :
      Repr Sign
      source
      @[instance_reducible]
      instance Float.Model.UnpackedFloat.instDecidableEqSign :
      DecidableEq Sign
      source
      @[instance_reducible]
      instance Float.Model.UnpackedFloat.Sign.instMul :
      Mul Sign
      source
      @[instance_reducible]
      instance Float.Model.UnpackedFloat.Sign.instDiv :
      Div Sign
      source
      @[instance_reducible]
      instance Float.Model.UnpackedFloat.Sign.instNeg :
      Neg Sign
      source
      @[instance_reducible]
      instance Float.Model.UnpackedFloat.Sign.instOrd :
      Ord Sign
      source
      def Float.Model.UnpackedFloat.Sign.apply (s : Sign) (n : Int) :
      Int

      Apply the given sign to the given integer.

      Instances For
        source
        def Float.Model.UnpackedFloat.Sign.toBitVec :
        Sign → BitVec 1

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

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

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

          Instances For