Overloading

[fmease]

Meta: Task: Expand.

Example:

data Nat: Type of
    zero: Nat
    succ: Nat -> Nat

use Nat.(zero succ)

data Fin: Nat -> Type of
    zero: Fin (succ zero)
    succ: '(n: Nat) -> Fin n -> Fin (succ n)

use Fin.(zero succ)

PROS: CONS: