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. The instance bodies delegate to the built-in operators (``+``, ``-``, ``*``, ``<``, ``<=``). Those builtins remain the primitive, SMT- interpreted operations; ``Num``/``Ord`` only add a typeclass surface on top of them. Because the methods are dictionary projections (opaque to the SMT backend) the classes are best used in ordinary computation rather than inside refinements that must reason about exact arithmetic — for that, keep using ``+``/``-`` directly. ── Classes ──────────────────────────────────────────────────────────── Num: addition, subtraction, multiplication.