[Agda] partial division property

Nils Anders Danielsson nad at chalmers.se
Mon Nov 5 14:48:03 CET 2012

On 2012-11-05 13:00, Serge D. Mechveliani wrote:
> Finally there appeared a report of that the checker expects  Set (max c l)
> for  ((q * b) ~~ a),  and this was a luck.

You may want to inspect the constraints (see the Agda menu).


More information about the Agda mailing list