After the Agda Reference Manual


module Modules.Parameterised where

open import Data.Nat

Module parameters

Modules may have parameters which are accessible inside the module.

The parameter can filled in outside of the module:


module X where

  module Y (x₁ : ℕ) where   -- parameter
    y₁ = suc x₁             -- using the parameter
    y₂ = suc y₁

  x₂ = suc (suc (Y.y₁ 10))  -- filling in the parameter
  x₂′ = suc (Y.y₂ 10)

Module application

One can define a new module by filling in a module parameter:


module X′ where

  module Y (x₁ : ℕ) where
    y₁ = suc x₁
    y₂ = suc y₁

  x₂ = suc (Y.y₂ 10)

  module Y′ = Y 10   -- module application

  x₂′ = suc Y′.y₂   -- usage

Opening with module application

Opening with module application:


module X″ where

  module Y (x₁ : ℕ) where
    y₁ = suc x₁
    y₂ = suc y₁

  x₂ = suc (Y.y₂ 10)

  open module Y′ = Y 10   -- opened module application

  x₂′ = suc y₂   -- usage

Mixing modifiers

Laws