Luke Palmer luqui

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