Skip to content

Instantly share code, notes, and snippets.

View andy0130tw's full-sized avatar
why no 🍆

Andy Pan andy0130tw

why no 🍆
View GitHub Profile
andy0130tw /
Last active August 20, 2020 17:09 — forked from L-TChen/
Fixing typos (?)

Intrinsically-typed de Bruijn representation of simply typed lambda calculus

open import Data.Nat
open import Data.Empty
  hiding (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality