class Actus.Amount (α : Type) extends Zero α, One α, Add α, Sub α, Mul α, Div α, Neg α, Min α, Max α, LE α : Type

Lawless numeric operations shared by the executable (Float) and the specification (ℝ) amount types. Definitions of the lending engine take [Amount α]; instantiate at Float to run and at ℝ to prove.

• zero : α
• one : α
• add : α → α → α
• sub : α → α → α
• mul : α → α → α
• div : α → α → α
• neg : α → α
• min : α → α → α
• max : α → α → α
• le : α → α → Prop
• abs : α → α

  Absolute value (magnitude).

@[implicit_reducible]

instance Actus.instAmountFloat : Amount Float

Executable instance: native IEEE-754 Float.

Equations

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

@[implicit_reducible]

noncomputable instance Actus.instAmountReal : Amount ℝ

Specification instance: the real numbers. Noncomputable (so it never leaks into the executable engine), with abs the Mathlib absolute value, so that Amount.abs (x : ℝ) = |x| definitionally and the order lemmas apply.

Equations

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

@[simp]

theorem Actus.Amount.abs_real (x : ℝ) : abs x = |x|