idris-lang/Idris-dev — pull request #937 by david-christiansen (2014-02-26 13:26:28+00:00)
Title: Postulate providers

Allow type providers to postulate their type, in addition to proving it.

Applications: easy interfacing to SMT solvers, compile-time quickcheck