[Agda] indices in record

Serge D. Mechveliani mechvel at botik.ru
Thu Sep 20 11:50:17 CEST 2012

A minor	note:

 record Insert (x : Nat) (xs : List Nat) (ord-xs : OrderedList? xs) : Set
     hd : Nat

is taken all right in  Agda-,
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"?).



More information about the Agda mailing list