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
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Float.Model.UnpackedFloat.instReprSign :
      Repr Sign
      Equations
      source
      def Float.Model.UnpackedFloat.instBEqSign.beq :
      Sign → Sign → Bool
      Equations
      Instances For
        source
        @[instance_reducible]
        instance Float.Model.UnpackedFloat.instBEqSign :
        BEq Sign
        Equations
        source
        @[instance_reducible]
        instance Float.Model.UnpackedFloat.Sign.instMul :
        Mul Sign
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[instance_reducible]
        instance Float.Model.UnpackedFloat.Sign.instDiv :
        Div Sign
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[instance_reducible]
        instance Float.Model.UnpackedFloat.Sign.instNeg :
        Neg Sign
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[instance_reducible]
        instance Float.Model.UnpackedFloat.Sign.instOrd :
        Ord Sign
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Float.Model.UnpackedFloat.Sign.apply (s : Sign) (n : Int) :
        Int

        Apply the given sign to the given integer.

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

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

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

            Equations
            Instances For