[Agda] Are the parameters implicit arguments to the constructors?

[Ulf Norell]

On Mon, Jun 16, 2008 at 5:28 PM, Andrés Sicard-Ramírez <
andres.sicard at gmail.com> wrote:

> Hi,
>
> I have the idea that the parameters are implicit arguments to the
> constructors. For example, the following code is type checked  (From
> Agda2/examples/AIM6/HelloAgda/Datatypes.agda)
>
> data List (A : Set) : Set where
>  []   : List A
>  _::_ : A -> List A -> List A
>
> nil : (A : Set) -> List A
> nil A = [] {A}
>
> but in
>
> foo : {A : Set} -> List A -> Bool
> foo ([] {A}) = {! !}
> foo (_::_ {A} x xs) = {! !}
>
> the first equation generates the error
>
> Is it the expected behavior?


Yes. In a right hand side you can pass the datatype parameters as implicit
arguments of a constructor, but they aren't stored with the constructor.
Hence, when pattern matching they aren't there for you to match on.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080616/61fcf241/attachment.html