[Agda] direct product for list

[Serge D. Mechveliani]

On Wed, Oct 10, 2012 at 10:44:16AM +0200, Andreas Abel wrote:
> Did you manage to fix this?  If not, you can send me the file with your  
> example and I can have a look again...

Please, replace respectively  Nat, ::,  <=,  _2
to their math symbols         \bn, \::, \<=, \_2
:
---------------------------------------------------
module Main where
open import Foreign.Haskell
open import IO.Primitive
open import Data.Unit using ( \top )
open import Data.Nat
open import Data.Product
open import Data.List
open import Prelude using ( toCostring )  -- by F. Kettelhoit

OrderedList? : List Nat -> Set
OrderedList? []             =  \top
OrderedList? (x :: [])      =  \top \times \top
OrderedList? (x :: y :: xs) =  x <= y \times (OrderedList? (y :: xs))

tailOrdered : {x : Nat} {xs : List Nat} -> OrderedList? (x :: xs) ->
                                                        OrderedList? xs
tailOrdered {xs = []} = proj_2
tailOrdered           = proj_2

main : IO Unit
main = putStrLn (toCostring "done")
---------------------------------------------------

The checker report is

/home/mechvel/haskell/agda/myPrograms/Main.agda:18,25-30
OrderedList? (.x Б┬╥ .xs) !=< нё _21 _22 of type Set
when checking that the expression projБ┌┌ has type
OrderedList? (.x Б┬╥ .xs) Б├▓ OrderedList? .xs

This is for  Agda-2.3.0.1, MAlonzo, lib-0.6.

Thanks,
Sergei



> On 08.10.12 12:59 PM, Serge D. Mechveliani wrote:
>> On Sun, Oct 07, 2012 at 11:49:36PM +0200, Andreas Abel wrote:
>>> On 07.10.12 4:49 PM, Serge D. Mechveliani wrote:
>> [..]
>>>> But then, I thought of the definition via the direct product (\times):
>>>>
>>>>   OrderedList'? : List Nat -> Set
>>>>   OrderedList'? []             =  \top
>>>>   OrderedList'? (x :: [])      =  \top \times \top
>>>>   OrderedList'? (x :: y :: xs) =  x <= y \times (OrderedList'? (y :: xs))

>>>>
>>>> It looks simpler, it does not introduce new constructors.
>>>> But I fail to process its data, so far. For example,
>>>>
>>>>   tailOrdered' : {x : Nat} {xs : List Nat} -> OrderedList'? (x :: xs) ->
>>>>                                                         OrderedList'? xs
>>>>   tailOrdered' = proj-2
>>>>
>>>> is not compiled:
[..]