structure Aesop.Percent : Type

• toFloat : Float

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.δ : 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 : Aesop.Percent

Equations

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

def Aesop.Percent.fifty : Aesop.Percent

Equations

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

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

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)