module Micro
import Data.String
An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if
- you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it;