Discussion:
Lists and products
(too old to reply)
Philip Wadler
2018-03-02 11:40:57 UTC
Permalink
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
Loading...