Ordinary notation for ExecFloat

Ordinary operators call the selected ExecFloat operations. Each instance requires the corresponding arithmetic or comparison capability. Formats whose values have a lawful total order provide their own LinearOrder.

@[instance_reducible]

instance FloatLib.Floats.execFloatAdd {F : Type u} [Numerics.EncodedFormat F] [ExecFloat.Backend.PolicyFor F] [ExecFloat.Add F] : Add (ExecFloat F)

+ is ordinary notation for the public format-selected addition capability.

@[instance_reducible]

instance FloatLib.Floats.execFloatSub {F : Type u} [Numerics.EncodedFormat F] [ExecFloat.Backend.PolicyFor F] [ExecFloat.Sub F] : Sub (ExecFloat F)

- is ordinary notation for the public format-selected subtraction capability.

@[instance_reducible]

instance FloatLib.Floats.execFloatMul {F : Type u} [Numerics.EncodedFormat F] [ExecFloat.Backend.PolicyFor F] [ExecFloat.Mul F] : Mul (ExecFloat F)

* is ordinary notation for the public format-selected multiplication capability.

@[instance_reducible]

instance FloatLib.Floats.execFloatDiv {F : Type u} [Numerics.EncodedFormat F] [ExecFloat.Backend.PolicyFor F] [ExecFloat.Div F] : Div (ExecFloat F)

/ is ordinary notation for the public format-selected division capability.

@[instance_reducible, instance 2000]

instance FloatLib.Floats.execFloatBEq {F : Type u} [Numerics.EncodedFormat F] [ExecFloat.Comparison F] : BEq (ExecFloat F)

== uses the format-defined comparison rather than structural code equality.