```
module Lang.other where
open import Lang.dataStructures renaming (_+_ to _⨦_)
open import Lang.functions using (_+_)
```

Modules are used to scope variable and function namespaces such as “packages” in languages like java or python. They behave as closures with the indentation as the indicator of the extent of the closure. Each Agda source file may contain one module at the top level. Modules can be imported as can be seen from the blocks of imports above.

Modules support nesting:

```
module nested where
module X where
= one
x₁
module Y where
= two
x₂
= X.x₁ + Y.x₂ sum
```

Importing modules:

```
open nested.X
= x₁ + one
x₁₁
open nested.Y renaming (x₂ to x₃)
= x₃ + one x₂
```

Modules can have parameters valid inside their closures:

```
module Sort (A : Set)(_≤_ : A → A → Bool) where
: A → List A → List A
insert = x :: []
insert x [] (y :: ys) with x ≤ y
insert x (y :: ys) | true = x :: y :: ys
insert x (y :: ys) | false = y :: insert x ys
insert x
: List A → List A
sort = []
sort [] (x :: xs) = insert x (sort xs) sort
```

Tuples are called as `Record`

s in Agda. Some examples are:

A tuple of `Bool`

and `ℕ`

:

```
record R : Set where
field
: Bool
r₁ : ℕ r₂
```

A generic tuple:

```
record Pair (A B : Set) : Set where
field
: A
fst : B snd
```

An object of `Pair`

can be constructed as:

```
: Pair ℕ ℕ
p23 = record { fst = two; snd = three } p23
```

The `constructor`

keyword can be specified to construct records:

```
record Pair' (A B : Set) : Set where
constructor _,_
field
: A
fst : B
snd
: Pair' ℕ ℕ
p45 = four , five p45
```

The values of a record can be pattern matched upon:

```
: Pair' ℕ ℕ → ℕ
left (x , y) = x left
```

A record can be parameterized:

```
record List' (A : Set) : Set where
constructor L
field
: ℕ
length : Vec A length
vector
: List' Bool
list₂ = L three vec3 list₂
```

All `Data`

definitions have an equivalent `Record`

definition, however `Record`

s are preferred whenever possible as a convention. Records have the obvious advantage of providing `getters`

and `setters`

for free.

`postulate`

s are another Agda language construct. These facilitate defining some type without the actual implementation.

```
postulate
: Set
A B : A
a : B
b _=AB=_ : A → B → Set
: a =AB= b a==b
```

```
data False : Set where
postulate bottom : False
```