Classes (kernel)

9.1 Class = record of functions

Class C τ ≡ { methods }

9.2 Instance = value

instance : Class C τ

Resolution is compile-time, not runtime.