[Agda] indices in record

[Serge D. Mechveliani]

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