# Implementation of floating-point numbers (experimental). #

def Int.shift2 (a : ) (b : ) :
Equations
Instances For
inductive FP.RMode :
Instances For
• prec :
• emax :
• precPos : 0 < FP.FloatCfg.prec
• precMax : FP.FloatCfg.prec FP.FloatCfg.emax
Instances
theorem FP.FloatCfg.precPos [self : FP.FloatCfg] :
0 < FP.FloatCfg.prec
theorem FP.FloatCfg.precMax [self : FP.FloatCfg] :
FP.FloatCfg.prec FP.FloatCfg.emax
Equations
• FP.prec = FP.FloatCfg.prec
Instances For
Equations
• FP.emax = FP.FloatCfg.emax
Instances For
Equations
• FP.emin = 1 - FP.FloatCfg.emax
Instances For
def FP.ValidFinite [C : FP.FloatCfg] (e : ) (m : ) :
Equations
• = (FP.emin e + FP.prec - 1 e + FP.prec - 1 FP.emax e = max (e + m.size - FP.prec) FP.emin)
Instances For
instance FP.decValidFinite [C : FP.FloatCfg] (e : ) (m : ) :
Equations
• = id inferInstance
inductive FP.Float [C : FP.FloatCfg] :
Instances For
def FP.Float.isFinite [C : FP.FloatCfg] :
FP.FloatBool
Equations
Instances For
def FP.toRat [C : FP.FloatCfg] (f : FP.Float) :
f.isFinite = true
Equations
Instances For
def FP.Float.zero [C : FP.FloatCfg] (s : Bool) :
FP.Float
Equations
Instances For
Equations
• FP.instInhabitedFloat = { default := }
def FP.Float.sign' [C : FP.FloatCfg] :
FP.Float
Equations
Instances For
def FP.Float.sign [C : FP.FloatCfg] :
FP.FloatBool
Equations
Instances For
def FP.Float.isZero [C : FP.FloatCfg] :
FP.FloatBool
Equations
Instances For
def FP.Float.neg [C : FP.FloatCfg] :
FP.FloatFP.Float
Equations
Instances For
def FP.divNatLtTwoPow (n : ) (d : ) :
Equations
Instances For
unsafe def FP.ofPosRatDn [C : FP.FloatCfg] (n : ℕ+) (d : ℕ+) :
FP.Float × Bool
Equations
• One or more equations did not get rendered due to their size.
Instances For
unsafe def FP.nextUpPos [C : FP.FloatCfg] (e : ) (m : ) (v : ) :
FP.Float
Equations
Instances For
unsafe def FP.nextDnPos [C : FP.FloatCfg] (e : ) (m : ) (v : ) :
FP.Float
Equations
• One or more equations did not get rendered due to their size.
Instances For
unsafe def FP.nextUp [C : FP.FloatCfg] :
FP.FloatFP.Float
Equations
Instances For
unsafe def FP.nextDn [C : FP.FloatCfg] :
FP.FloatFP.Float
Equations
Instances For
unsafe def FP.ofRatUp [C : FP.FloatCfg] :
FP.Float
Equations
• One or more equations did not get rendered due to their size.
Instances For
unsafe def FP.ofRatDn [C : FP.FloatCfg] (r : ) :
FP.Float
Equations
Instances For
unsafe def FP.ofRat [C : FP.FloatCfg] :
FP.RModeFP.Float
Equations
• One or more equations did not get rendered due to their size.
Instances For
instance FP.Float.instNeg [C : FP.FloatCfg] :
Neg FP.Float
Equations
• FP.Float.instNeg = { neg := FP.Float.neg }
unsafe def FP.Float.add [C : FP.FloatCfg] (mode : FP.RMode) :
FP.FloatFP.FloatFP.Float
Equations
• One or more equations did not get rendered due to their size.
Instances For
unsafe instance FP.Float.instAdd [C : FP.FloatCfg] :
Equations
unsafe def FP.Float.sub [C : FP.FloatCfg] (mode : FP.RMode) (f1 : FP.Float) (f2 : FP.Float) :
FP.Float
Equations
Instances For
unsafe instance FP.Float.instSub [C : FP.FloatCfg] :
Sub FP.Float
Equations
• FP.Float.instSub = { sub := }
unsafe def FP.Float.mul [C : FP.FloatCfg] (mode : FP.RMode) :
FP.FloatFP.FloatFP.Float
Equations
• One or more equations did not get rendered due to their size.
Instances For
unsafe def FP.Float.div [C : FP.FloatCfg] (mode : FP.RMode) :
FP.FloatFP.FloatFP.Float
Equations
• One or more equations did not get rendered due to their size.
Instances For