[Agda] Level constraints

Nils Anders Danielsson nad at cse.gu.se
Thu Nov 14 19:43:21 CET 2013

On 2013-11-14 16:34, Christian Sattler wrote:
> What do you think?

There are many options (at least if we restrict the discussion to

* The status quo.

* Something like what you suggest.

* Some kind of cumulativity.

* Conor's lifting primitive (Crude but Effective Stratification,

* Allowing the solver to produce non-unique solutions. (I believe that
   Mattieu has implemented something like this for Coq.)

* …

I think it would be interesting to see a careful discussion of the pros
and cons of these different designs.


More information about the Agda mailing list