[Agda] Lists and products

[Philip Wadler]

And now a simpler question.

In order to make it handy to write examples with lists, it is handy to
define:

[_] <https://wenkokke.github.io/Lists#2988> : ∀ {A
<https://wenkokke.github.io/Lists#2997> : Set} → A
<https://wenkokke.github.io/Lists#2997> → List
<https://wenkokke.github.io/Lists#813> A
<https://wenkokke.github.io/Lists#2997>[
<https://wenkokke.github.io/Lists#2988> z
<https://wenkokke.github.io/Lists#3021> ]
<https://wenkokke.github.io/Lists#2988> = z
<https://wenkokke.github.io/Lists#3021> ∷
<https://wenkokke.github.io/Lists#856> []
<https://wenkokke.github.io/Lists#842>
[_,_] <https://wenkokke.github.io/Lists#3035> : ∀ {A
<https://wenkokke.github.io/Lists#3046> : Set} → A
<https://wenkokke.github.io/Lists#3046> → A
<https://wenkokke.github.io/Lists#3046> → List
<https://wenkokke.github.io/Lists#813> A
<https://wenkokke.github.io/Lists#3046>[
<https://wenkokke.github.io/Lists#3035> y
<https://wenkokke.github.io/Lists#3074> ,
<https://wenkokke.github.io/Lists#3035> z
<https://wenkokke.github.io/Lists#3078> ]
<https://wenkokke.github.io/Lists#3035> = y
<https://wenkokke.github.io/Lists#3074> ∷
<https://wenkokke.github.io/Lists#856> z
<https://wenkokke.github.io/Lists#3078> ∷
<https://wenkokke.github.io/Lists#856> []
<https://wenkokke.github.io/Lists#842>
[_,_,_] <https://wenkokke.github.io/Lists#3096> : ∀ {A
<https://wenkokke.github.io/Lists#3109> : Set} → A
<https://wenkokke.github.io/Lists#3109> → A
<https://wenkokke.github.io/Lists#3109> → A
<https://wenkokke.github.io/Lists#3109> → List
<https://wenkokke.github.io/Lists#813> A
<https://wenkokke.github.io/Lists#3109>[
<https://wenkokke.github.io/Lists#3096> x
<https://wenkokke.github.io/Lists#3141> ,
<https://wenkokke.github.io/Lists#3096> y
<https://wenkokke.github.io/Lists#3145> ,
<https://wenkokke.github.io/Lists#3096> z
<https://wenkokke.github.io/Lists#3149> ]
<https://wenkokke.github.io/Lists#3096> = x
<https://wenkokke.github.io/Lists#3141> ∷
<https://wenkokke.github.io/Lists#856> y
<https://wenkokke.github.io/Lists#3145> ∷
<https://wenkokke.github.io/Lists#856> z
<https://wenkokke.github.io/Lists#3149> ∷
<https://wenkokke.github.io/Lists#856> []
<https://wenkokke.github.io/Lists#842>
[_,_,_,_] <https://wenkokke.github.io/Lists#3171> : ∀ {A
<https://wenkokke.github.io/Lists#3186> : Set} → A
<https://wenkokke.github.io/Lists#3186> → A
<https://wenkokke.github.io/Lists#3186> → A
<https://wenkokke.github.io/Lists#3186> → A
<https://wenkokke.github.io/Lists#3186> → List
<https://wenkokke.github.io/Lists#813> A
<https://wenkokke.github.io/Lists#3186>[
<https://wenkokke.github.io/Lists#3171> w
<https://wenkokke.github.io/Lists#3222> ,
<https://wenkokke.github.io/Lists#3171> x
<https://wenkokke.github.io/Lists#3226> ,
<https://wenkokke.github.io/Lists#3171> y
<https://wenkokke.github.io/Lists#3230> ,
<https://wenkokke.github.io/Lists#3171> z
<https://wenkokke.github.io/Lists#3234> ]
<https://wenkokke.github.io/Lists#3171> = w
<https://wenkokke.github.io/Lists#3222> ∷
<https://wenkokke.github.io/Lists#856> x
<https://wenkokke.github.io/Lists#3226> ∷
<https://wenkokke.github.io/Lists#856> y
<https://wenkokke.github.io/Lists#3230> ∷
<https://wenkokke.github.io/Lists#856> z
<https://wenkokke.github.io/Lists#3234> ∷
<https://wenkokke.github.io/Lists#856> []
<https://wenkokke.github.io/Lists#842>
[_,_,_,_,_] <https://wenkokke.github.io/Lists#3260> : ∀ {A
<https://wenkokke.github.io/Lists#3277> : Set} → A
<https://wenkokke.github.io/Lists#3277> → A
<https://wenkokke.github.io/Lists#3277> → A
<https://wenkokke.github.io/Lists#3277> → A
<https://wenkokke.github.io/Lists#3277> → A
<https://wenkokke.github.io/Lists#3277> → List
<https://wenkokke.github.io/Lists#813> A
<https://wenkokke.github.io/Lists#3277>[
<https://wenkokke.github.io/Lists#3260> v
<https://wenkokke.github.io/Lists#3317> ,
<https://wenkokke.github.io/Lists#3260> w
<https://wenkokke.github.io/Lists#3321> ,
<https://wenkokke.github.io/Lists#3260> x
<https://wenkokke.github.io/Lists#3325> ,
<https://wenkokke.github.io/Lists#3260> y
<https://wenkokke.github.io/Lists#3329> ,
<https://wenkokke.github.io/Lists#3260> z
<https://wenkokke.github.io/Lists#3333> ]
<https://wenkokke.github.io/Lists#3260> = v
<https://wenkokke.github.io/Lists#3317> ∷
<https://wenkokke.github.io/Lists#856> w
<https://wenkokke.github.io/Lists#3321> ∷
<https://wenkokke.github.io/Lists#856> x
<https://wenkokke.github.io/Lists#3325> ∷
<https://wenkokke.github.io/Lists#856> y
<https://wenkokke.github.io/Lists#3329> ∷
<https://wenkokke.github.io/Lists#856> z
<https://wenkokke.github.io/Lists#3333> ∷
<https://wenkokke.github.io/Lists#856> []
<https://wenkokke.github.io/Lists#842>
[_,_,_,_,_,_] <https://wenkokke.github.io/Lists#3363> : ∀ {A
<https://wenkokke.github.io/Lists#3382> : Set} → A
<https://wenkokke.github.io/Lists#3382> → A
<https://wenkokke.github.io/Lists#3382> → A
<https://wenkokke.github.io/Lists#3382> → A
<https://wenkokke.github.io/Lists#3382> → A
<https://wenkokke.github.io/Lists#3382> → A
<https://wenkokke.github.io/Lists#3382> → List
<https://wenkokke.github.io/Lists#813> A
<https://wenkokke.github.io/Lists#3382>[
<https://wenkokke.github.io/Lists#3363> u
<https://wenkokke.github.io/Lists#3426> ,
<https://wenkokke.github.io/Lists#3363> v
<https://wenkokke.github.io/Lists#3430> ,
<https://wenkokke.github.io/Lists#3363> w
<https://wenkokke.github.io/Lists#3434> ,
<https://wenkokke.github.io/Lists#3363> x
<https://wenkokke.github.io/Lists#3438> ,
<https://wenkokke.github.io/Lists#3363> y
<https://wenkokke.github.io/Lists#3442> ,
<https://wenkokke.github.io/Lists#3363> z
<https://wenkokke.github.io/Lists#3446> ]
<https://wenkokke.github.io/Lists#3363> = u
<https://wenkokke.github.io/Lists#3426> ∷
<https://wenkokke.github.io/Lists#856> v
<https://wenkokke.github.io/Lists#3430> ∷
<https://wenkokke.github.io/Lists#856> w
<https://wenkokke.github.io/Lists#3434> ∷
<https://wenkokke.github.io/Lists#856> x
<https://wenkokke.github.io/Lists#3438> ∷
<https://wenkokke.github.io/Lists#856> y
<https://wenkokke.github.io/Lists#3442> ∷
<https://wenkokke.github.io/Lists#856> z
<https://wenkokke.github.io/Lists#3446> ∷
<https://wenkokke.github.io/Lists#856> []
<https://wenkokke.github.io/Lists#842>

This conflicts (in terms of parsing) with the standard notation for
products, so I have altered that slightly:

open import Data.Product
<https://agda.github.io/agda-stdlib/Data.Product.html> using (_×_
<https://agda.github.io/agda-stdlib/Data.Product.html#1329>) renaming
(_,_ <https://agda.github.io/agda-stdlib/Data.Product.html#543> to
⟨_,_⟩ <https://agda.github.io/agda-stdlib/Data.Product.html#543>)

The question is, have I chosen the best way to deal with the situation? Or
is there an alternative that others recommend? Cheers, -- P


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180302/4bcbcadd/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180302/4bcbcadd/attachment-0001.ksh>