Skip to content

Instantly share code, notes, and snippets.

@gallais
gallais / UntypedLambda.agda
Created September 7, 2015 18:53
Interpreting the untyped lambda calculus in Agda
{-# OPTIONS --copatterns #-}
module UntypedLambda where
open import Size
open import Function
mutual
data Delay (A : Set) (i : Size) : Set where