[Agda] Newbie questions after reading Dependently Typed Programming in Agda

[Nils Anders Danielsson]

On 2010-10-12 23:46, Thorsten Altenkirch wrote:
>> Is the type checker aware that True and False
>> are the only valid types from isTrue?
>
> Nope.

Agda identifies isTrue as a "constructor-headed function", and given the
constraint "isTrue ?0 = False" the meta-variable ?0 is inferred to be
false:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments

I'm not sure if this is related to the question, though.

> You only dot if you repeat variables.

No, you can dot constructors (and general expressions).

--
/NAD