{- Agda modules. Crash course. -} -- Each Agda file contains a single top-level module with -- the same name as the file. module Modules where -- importing gives you access to modules defined in other files -- opening lets you use the names from the module unqualified open import Data.Bool -- defined in Data/Bool.agda open import Data.List -- Parameterized modules are similar to Coq sections. module Sort {A : Set}(_≤_ : A → A → Bool) where insert : A → List A → List A insert y [] = y ∷ [] insert y (x ∷ xs) = if y ≤ x then y ∷ x ∷ xs else x ∷ insert y xs sort : List A → List A sort [] = [] sort (x ∷ xs) = insert x (sort xs) -- Now let's sort something! -- This is a wrapper module for Data.Nat from the standard library -- that defines boolean _≤_ and _≥_. open import Nat -- We can instantiate the parameters of a parameterized module -- (the A parameter is implicit) open Sort _≤_ -- Now sort : List ℕ → List ℕ xs = 3 ∷ 7 ∷ 0 ∷ 10 ∷ 2 ∷ [] test₁ = sort xs -- using the non-instantiated sort test₂ = Sort.sort _≥_ xs -- We might want to give a nicer name to Sort.sort open Sort using () renaming (sort to sortBy) test₃ = sortBy _≥_ xs