[Agda] question on `Any'

Nils Anders Danielsson nad at cse.gu.se
Mon Aug 19 21:57:40 CEST 2013

On 2013-08-13 14:34, Dominique Devriese wrote:
> For more info, see the Agda tutorial by Norell and Chapman for
> example.  They mention the following rule:
>     The rule for when an argument should be dotted is: if there is a unique
>     type correct value for the argument it should be dotted.

This rule is rather imprecise. Unique with respect to what notion of
equality? Certainly not propositional equality.


More information about the Agda mailing list