justified-type-inference

An implementation of Compositional type inference in Idris with a complete proof

I am now working on a Coq version of this because of a code generation bug in Idris and because typechecking was so slow.