[Agda] Lists and products

Discussion:

Philip Wadler

2018-03-02 11:40:57 UTC

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/

Guillaume Allais

2018-03-02 11:51:16 UTC

Permalink

Hi Phil, instead of declaring all of these toplevel definitions
with different arities, you can use infix identifiers. Even better:
using pattern-synonyms you'll be able to use these on the left
hand side!

=================================================
module poc.list-literals where

open import Agda.Builtin.List

module _ {â} {A : Set â} where

Â infix 1 [_
Â infixr 2 _,_
Â infix 3 _]

Â -- [_ : List A â List A
Â pattern [_ xs = xs

Â -- _,_ : A â List A â List A
Â pattern _,_ a as = a â· as

Â --Â _] : A â List A
Â pattern _] x = x â· []

open import Agda.Builtin.Nat

_ : List Nat
_ = [ 1 , 2 , 3 , 4 ]

open import Data.Maybe

last : List Nat â Maybe Nat
last ([ x ])Â = just x
last (x â· xs) = last xs
last _ = nothing
=================================================

Post by Philip Wadler
And now a simpler question.
In order to make it handy to write examples with lists, it is handy to
[_] <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
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/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

Philip Wadler

2018-03-02 12:07:20 UTC

Permalink

Guillaume,

Thank you for the suggestion. I tried something similar, but gave it up
because I wanted to write

map (1 +_) [ 0 , 1 , 2 ]

rather than

map (1 +_) ([ 0 , 1 , 2 ])

in examples. Thank you for the point about 'pattern', which should apply to
either method. Thank you also for the example of using `_` to name an
example, which I had not seen before and is much more convenient than using
ex1, ex2, ..., which may need to be renamed if other examples are added in
the middle.

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/

Post by Guillaume Allais
Hi Phil, instead of declaring all of these toplevel definitions
using pattern-synonyms you'll be able to use these on the left
hand side!
=================================================
module poc.list-literals where
open import Agda.Builtin.List
module _ {â} {A : Set â} where
infix 1 [_
infixr 2 _,_
infix 3 _]
-- [_ : List A â List A
pattern [_ xs = xs
-- _,_ : A â List A â List A
pattern _,_ a as = a â· as
-- _] : A â List A
pattern _] x = x â· []
open import Agda.Builtin.Nat
_ : List Nat
_ = [ 1 , 2 , 3 , 4 ]
open import Data.Maybe
last : List Nat â Maybe Nat
last ([ x ]) = just x
last (x â· xs) = last xs
last _ = nothing
=================================================
And now a simpler question.
In order to make it handy to write examples with lists, it is handy to
[_] <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
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/
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
_______________________________________________
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda