Agda Essentials

Here we describe some of the essential concepts and syntax of the Agda programming language and proof assistant. The goal is to provide some background for readers who are not already familiar with Agda, to help them understand the other sections of the specification. For more details, the reader is encouraged to consult the official Agda documentation .

{-# OPTIONS --safe #-}

module EssentialAgda where

open import Prelude using (Type)
open import Data.Nat

Record Types

A record is a product with named accessors for the individual fields. It provides a way to define a type that groups together inhabitants of other types. Example.

record Pair (A B : Type) : Type where
  constructor ⦅_,_⦆
  field
    fst : A
    snd : B

We can construct an element of the type Pair ℕ ℕ (i.e., a pair of natural numbers) as follows:

p23 : Pair ℕ ℕ
p23 = record { fst = ; snd =  }

Since our definition of the Pair type provides an (optional) constructor ⦅_,_⦆, we can have defined p23 as follows:

p23' : Pair ℕ ℕ
p23' = ⦅  ,  ⦆

Finally, we can “update” a record by deriving from it a new record whose fields may contain new values. The syntax is best explained by way of example.

p24 : Pair ℕ ℕ
p24 = record p23 { snd =  }

This results a new record, p24, which denotes the pair ⦅ , ⦆.  See also agda.readthedocs.io/record-types.