[Agda] `let' in record decl

[Andreas Abel]

Hi Sergei,

On 09.10.12 3:29 PM, Serge D. Mechveliani wrote:
> Please, how to abbreviate  `Carrier ord'  in the declaration  of
> ------------------------------------
> record Merge1
>    {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2)
>    (m : Carrier ord) (xs : List $ Carrier ord) (ys : List $ Carrier ord)
>                                          : Set (suc $ max c $ max l1 l2)
>    where
>    A = Carrier ord
>    field list    : List A
>          ordered : OrderedList? ord (m :: list)
> ------------------------------------
> ?
> (Agda-2.3.0.1, MAlonzo).
>
> After `where', it works  `A = Carrier ord'.
> But how to abbreviate the previous three occurences?

That is unfortunately not possible.  In a telescope (the bindings 
between "Merge1" and ": Set...") one cannot use let in Agda (although it 
would not be unthinkable).


> Question 2.
> (suc $ max c $ max l1 l2) : Level
> comes from my declaration of the type  OrderedList?
> -- where this expression is copied from  DecTotalOrder
> (of Standard Library lib-0.6), without understanding of how the levels
> must be set.
> Now, what level needs to be set for  record Merge1  ?

Try putting a question mark and see what levels are accepted.

Cheers,
Andreas

-- 
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/