structure Aesop.Percent : Type

• toFloat : Float

instance Aesop.instInhabitedPercent : Inhabited Percent

Equations

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

def Aesop.Percent.ofFloat (f : Float) : Option 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 Percent

Equations

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

@[inline]

def Aesop.Percent.δ : Percent

Equations

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

instance Aesop.Percent.instBEq : BEq Percent

Equations

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

instance Aesop.Percent.instOrd : Ord 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 Percent

Equations

• Aesop.Percent.instLT = ltOfOrd

instance Aesop.Percent.instLE : LE Percent

Equations

• Aesop.Percent.instLE = leOfOrd

instance Aesop.Percent.instToString : ToString Percent

Equations

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

instance Aesop.Percent.instHPowNat : HPow Percent Nat 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 : Percent

Equations

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

def Aesop.Percent.fifty : Percent

Equations

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

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

Equations

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

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

Equations

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