Num

Numeric and ordering typeclasses (Lean-style, dictionary-passing). These classes give *named, type-directed* access to arithmetic and comparison for the primitive numeric types. Method calls such as ``add x y`` resolve automatically to the instance selected by the argument types — ``Num Int`` for integers, ``Num Float`` for floats. Every method specifies its relationship to the primitive SMT operations. Instances must satisfy those refinements, and callers (including generic functions with [Num a] / [Ord a]) can use the checked result guarantees. The operators remain available directly inside refinement predicates. ── Classes ──────────────────────────────────────────────────────────── Num: addition, subtraction, multiplication.
Table of Contents

Types

Num

(inductive)
Num: addition, subtraction, multiplication.
inductive Num a

Ord

(inductive)
Ord: ordering comparisons. ``gt``/``geq`` have default bodies derived from ``lt``/``leq``, so instances only need to provide the latter two.
inductive Ord a

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

Num (inductive)

mk

constructor
Num: addition, subtraction, multiplication.
(Num a)

Ord (inductive)

mk

constructor
Ord: ordering comparisons. ``gt``/``geq`` have default bodies derived from ``lt``/``leq``, so instances only need to provide the latter two.
(Ord a)

Functions

add

def add ∀a:Β (_d4598 : (Num a)) (x : a) (y : a) : {r : a | r = x + y}

sub

def sub ∀a:Β (_d4599 : (Num a)) (x : a) (y : a) : {r : a | r = x - y}

mul

def mul ∀a:Β (_d4600 : (Num a)) (x : a) (y : a) : {r : a | r = x * y}

lt

def lt ∀a:Β (_d4601 : (Ord a)) (x : a) (y : a) : {r : Bool | r = x < y}

leq

def leq ∀a:Β (_d4602 : (Ord a)) (x : a) (y : a) : {r : Bool | r = x ≤ y}

gt

def gt ∀a:Β (_d4603 : (Ord a)) (x : a) (y : a) : {r : Bool | r = x > y}

geq

def geq ∀a:Β (_d4604 : (Ord a)) (x : a) (y : a) : {r : Bool | r = x ≥ y}