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

Equations

• Aesop.Percent.instMulPercent = { mul := fun p q => { toFloat := p.toFloat * q.toFloat } }

@[inline]

def Aesop.Percent.δ : Aesop.Percent

Equations

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

instance Aesop.Percent.instBEqPercent : BEq Aesop.Percent

Equations

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

instance Aesop.Percent.instOrdPercent : Ord Aesop.Percent

Equations

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

instance Aesop.Percent.instLTPercent : LT Aesop.Percent

Equations

• Aesop.Percent.instLTPercent = ltOfOrd

instance Aesop.Percent.instLEPercent : LE Aesop.Percent

Equations

• Aesop.Percent.instLEPercent = leOfOrd

instance Aesop.Percent.instToStringPercent : ToString Aesop.Percent

Equations

• Aesop.Percent.instToStringPercent = { toString := fun p => toString p.toFloat }

instance Aesop.Percent.instHPowPercentNat : HPow Aesop.Percent Nat Aesop.Percent

Equations

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

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 (Nat.toFloat n / 100)