Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.

{-# OPTIONS --without-K --safe #-}

module prelude where

open import general-notation public
open import empty-type public
open import unit-type public
open import binary-sums public
open import binary-products public
open import sums public
open import products public
open import identity-type public
open import natural-numbers-type public
open import Bool public
open import List public
open import Vector public

Go back to the table of contents