Andy Pan andy0130tw

🍌

why no 🍆

Write code to explore any possibilities, not to seek the answers, but to understand the questions. /* FOSS collection: @qbane */

andy0130tw / FLOLAC-STLC.lagda.md

Last active August 20, 2020 17:09 — forked from L-TChen/FLOLAC-STLC.lagda.md

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