← Docs

Modules

Top-level \import and \export. Definitions are private by default.

\import

\import nat

It imports all expose definitions in module nat.

\export

\export Nat add

As you can see, we will expose inductive types as a bundle, if we expose Nat, then also Nat/zero, Nat/suc, and Nat/elim.

Example: a small module

\export Nat add

\data Nat : 𝓤
  | zero : Nat
  | suc : Nat -> Nat

\let add : (m n : Nat) -> Nat \where
  add m n <= \elim m
  | add zero n => n
  | add (suc m) n => suc (add m n)