Parsing telescopes [Re: [Agda] indices in record]

[Andreas Abel]

The parse rule is

   record identifier telescope : type where

and a telescope is a sequence of bindings

   (identifier : type)  or
   {identifier : type}  or
   identifier           or
   {identifier}         or ...

but the identifier can never be dropped, this would lead to ambiguities, 
like in

   record R A : Set where

with the interpretations

   R : A -> Set   (not what Agda sees)
   R : (A : _) -> Set (what Agda sees).

If you want to drop the identifier, you can use _, like in

   ... (_ : OrderedList? xs)

Cheers,
Andreas

On 20.09.2012 11:50, Serge D. Mechveliani wrote:
> A minor	note:
>
>   record Insert (x : Nat) (xs : List Nat) (ord-xs : OrderedList? xs) : Set
>     where
>     field
>       hd : Nat
>       ...
>
> is taken all right in  Agda-2.3.0.1,
> and removing  "ord-x : "  in the first line leads to the report
>
>    " Parse error  ... ) : Set  ".
>
> Probably, it is better to explicitly report something like
>                            "No index for the 3-rd argument type ..."
>
> -- if the language does indeed require such (is this called "index"?).
>
> Regards,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/