dtlc Dependently typed lambda calculus - Practice with DTT Done Basic DT stuffs (with built-in nat) Product Sum Type Implicit Arguments Inductive Type