STLC Try to implement a STLC REPL in Coq & Haskell. Formalized in Coq, Run in Haskell. TODO Formally verify some feature of this implementation in Coq De bruijn Index