[Agda] Lists and products

[Guillaume Allais]

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

On 02/03/18 12:40, Philip Wadler wrote:
> 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/
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180302/a3132141/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180302/a3132141/attachment-0001.sig>