Documentation

Aesop.Percent

structure Aesop.Percent :

toFloat : Float

Instances For

instance Aesop.instInhabitedPercent :

Inhabited Aesop.Percent

Equations

Aesop.instInhabitedPercent = { default := { toFloat := default } }

def Aesop.Percent.ofFloat (f : Float) :

Option Aesop.Percent

Equations

Aesop.Percent.ofFloat f = if (decide (0 ≤ f) && decide (f ≤ 1.0)) = true then some { toFloat := f } else none

instance Aesop.Percent.instMul :

Mul Aesop.Percent

Equations

Aesop.Percent.instMul = { mul := fun (p q : Aesop.Percent) => { toFloat := p.toFloat * q.toFloat } }

@[inline]

def Aesop.Percent.δ :

Equations

Aesop.Percent.δ = { toFloat := 1e-5 }

instance Aesop.Percent.instBEq :

BEq Aesop.Percent

Equations

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

instance Aesop.Percent.instOrd :

Ord Aesop.Percent

Equations

Aesop.Percent.instOrd = { compare := fun (p q : Aesop.Percent) => if (p == q) = true then Ordering.eq else if p.toFloat < q.toFloat then Ordering.lt else Ordering.gt }

instance Aesop.Percent.instLT :

LT Aesop.Percent

Equations

Aesop.Percent.instLT = ltOfOrd

instance Aesop.Percent.instLE :

LE Aesop.Percent

Equations

Aesop.Percent.instLE = leOfOrd

instance Aesop.Percent.instToString :

ToString Aesop.Percent

Equations

Aesop.Percent.instToString = { toString := fun (p : Aesop.Percent) => toString p.toFloat }

instance Aesop.Percent.instHPowNat :

HPow Aesop.Percent Nat Aesop.Percent

Equations

Aesop.Percent.instHPowNat = { hPow := fun (x : Aesop.Percent) (x_1 : Nat) => match x, x_1 with | { toFloat := p }, n => { toFloat := p ^ n.toFloat } }

def Aesop.Percent.hundred :

Equations

Aesop.Percent.hundred = { toFloat := 1 }

def Aesop.Percent.fifty :

Equations

Aesop.Percent.fifty = { toFloat := 0.5 }

def Aesop.Percent.toHumanString (p : Aesop.Percent) :

Equations

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

def Aesop.Percent.ofNat (n : Nat) :

Option Aesop.Percent

Equations

Aesop.Percent.ofNat n = Aesop.Percent.ofFloat (n.toFloat / 100)