Skip to content

Instantly share code, notes, and snippets.

@gergoerdi
Created August 17, 2012 08:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gergoerdi/3376887 to your computer and use it in GitHub Desktop.
Save gergoerdi/3376887 to your computer and use it in GitHub Desktop.
Untyped lambda-calculus
module Lambda where
open import Data.Nat
open import Data.Fin
data Exp : ℕ → Set where
Var : {n : ℕ} → Fin n → Exp n
Lam : {n : ℕ} → Exp (suc n) → Exp n
_·_ : {n m : ℕ} → Exp n → Exp m → Exp (n ⊓ m)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment