Skip to content

Files

Latest commit

a6ab4f3 · Apr 2, 2019

History

History
4 lines (3 loc) · 286 Bytes

README.md

File metadata and controls

4 lines (3 loc) · 286 Bytes

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.