Skip to content

Instantly share code, notes, and snippets.

View joeycapper's full-sized avatar

Joey Capper joeycapper

View GitHub Profile
@joeycapper
joeycapper / FpAtLunch.agda
Last active January 16, 2018 14:44
Some of the dependent types we discussed today in Agda
module FpAtLunch where
open import Data.Nat
open import Data.Bool
---------------------------------
-- Lists of length n (Vectors) --
---------------------------------
-- In Agda `Set` is used to denote the type of types (rather than `Type` or `*`)