11Kilobytes

data Ty : Set
data Tm : Ty → Set

postulate Var : Ty → Set

data Ty where
  pi sg : (A : Ty)(B : Var A → Ty) → Ty

data Subst {A} : (Var A → Ty) → Tm A → Ty → Set where
  -- need to fill this in

11Kilobytes

Programming Achievements: How to Level Up as a Developer

This gist is part of a blog post. Check it out at:

http://jasonrudolph.com/blog/2011/08/09/programming-achievements-how-to-level-up-as-a-developer