<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<tt>Hi Phil, instead of declaring all of these toplevel definitions<br>
with different arities, you can use infix identifiers. Even
better:<br>
using pattern-synonyms you'll be able to use these on the left<br>
hand side!<br>
<br>
</tt><tt><tt>=================================================<br>
</tt>module poc.list-literals where<br>
<br>
open import Agda.Builtin.List<br>
<br>
module _ {ℓ} {A : Set ℓ} where<br>
<br>
infix 1 [_<br>
infixr 2 _,_<br>
infix 3 _]<br>
<br>
-- [_ : List A → List A<br>
pattern [_ xs = xs<br>
<br>
-- _,_ : A → List A → List A<br>
pattern _,_ a as = a ∷ as<br>
<br>
-- _] : A → List A<br>
pattern _] x = x ∷ []<br>
<br>
<br>
open import Agda.Builtin.Nat<br>
<br>
_ : List Nat<br>
_ = [ 1 , 2 , 3 , 4 ]<br>
<br>
open import Data.Maybe<br>
<br>
last : List Nat → Maybe Nat<br>
last ([ x ]) = just x<br>
last (x ∷ xs) = last xs<br>
last _ = nothing<br>
=================================================<br>
</tt><br>
<div class="moz-cite-prefix">On 02/03/18 12:40, Philip Wadler wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAESRbcoSn4TdDJGd9vcE0_RiGib-J9mFDriJc1EK6wSvdh=UGg@mail.gmail.com">
<div dir="ltr">
<div>And now a simpler question.</div>
<div><br>
</div>
<div>In order to make it handy to write examples with lists, it
is handy to define:</div>
<div><br>
</div>
<div>
<pre class="gmail-Agda" style="margin:0px 0px 15px;padding:0.4em;font-size:0.85em;border:1px solid rgb(201,225,246);border-radius:3px;background:rgb(232,242,251);overflow-x:auto;font-family:Consolas,Menlo,Monaco,"Lucida Console","Liberation Mono","DejaVu Sans Mono","Bitstream Vera Sans Mono","Courier New",monospace,serif;color:rgb(17,17,17);font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><a id="gmail-2988" href="https://wenkokke.github.io/Lists#2988" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[_]</a> <a id="gmail-2992" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-2994" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">∀</a> <a id="gmail-2996" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">{</a><a id="gmail-2997" href="https://wenkokke.github.io/Lists#2997" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-2999" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3001" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none" moz-do-not-send="true">Set</a><a id="gmail-3004" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">}</a> <a id="gmail-3006" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3008" href="https://wenkokke.github.io/Lists#2997" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3010" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3012" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">List</a> <a id="gmail-3017" href="https://wenkokke.github.io/Lists#2997" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a>
<a id="gmail-3019" href="https://wenkokke.github.io/Lists#2988" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[</a> <a id="gmail-3021" href="https://wenkokke.github.io/Lists#3021" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3023" href="https://wenkokke.github.io/Lists#2988" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">]</a> <a id="gmail-3025" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">=</a> <a id="gmail-3027" href="https://wenkokke.github.io/Lists#3021" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3029" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3031" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[]</a>
<a id="gmail-3035" href="https://wenkokke.github.io/Lists#3035" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[_,_]</a> <a id="gmail-3041" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3043" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">∀</a> <a id="gmail-3045" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">{</a><a id="gmail-3046" href="https://wenkokke.github.io/Lists#3046" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3048" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3050" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none" moz-do-not-send="true">Set</a><a id="gmail-3053" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">}</a> <a id="gmail-3055" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3057" href="https://wenkokke.github.io/Lists#3046" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3059" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3061" href="https://wenkokke.github.io/Lists#3046" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3063" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3065" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">List</a> <a id="gmail-3070" href="https://wenkokke.github.io/Lists#3046" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a>
<a id="gmail-3072" href="https://wenkokke.github.io/Lists#3035" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[</a> <a id="gmail-3074" href="https://wenkokke.github.io/Lists#3074" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3076" href="https://wenkokke.github.io/Lists#3035" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3078" href="https://wenkokke.github.io/Lists#3078" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3080" href="https://wenkokke.github.io/Lists#3035" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">]</a> <a id="gmail-3082" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">=</a> <a id="gmail-3084" href="https://wenkokke.github.io/Lists#3074" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3086" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3088" href="https://wenkokke.github.io/Lists#3078" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3090" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3092" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[]</a>
<a id="gmail-3096" href="https://wenkokke.github.io/Lists#3096" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[_,_,_]</a> <a id="gmail-3104" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3106" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">∀</a> <a id="gmail-3108" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">{</a><a id="gmail-3109" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3111" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3113" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none" moz-do-not-send="true">Set</a><a id="gmail-3116" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">}</a> <a id="gmail-3118" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3120" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3122" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3124" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3126" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3128" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3130" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3132" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">List</a> <a id="gmail-3137" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a>
<a id="gmail-3139" href="https://wenkokke.github.io/Lists#3096" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[</a> <a id="gmail-3141" href="https://wenkokke.github.io/Lists#3141" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3143" href="https://wenkokke.github.io/Lists#3096" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3145" href="https://wenkokke.github.io/Lists#3145" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3147" href="https://wenkokke.github.io/Lists#3096" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3149" href="https://wenkokke.github.io/Lists#3149" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3151" href="https://wenkokke.github.io/Lists#3096" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">]</a> <a id="gmail-3153" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">=</a> <a id="gmail-3155" href="https://wenkokke.github.io/Lists#3141" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3157" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3159" href="https://wenkokke.github.io/Lists#3145" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3161" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3163" href="https://wenkokke.github.io/Lists#3149" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3165" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3167" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[]</a>
<a id="gmail-3171" href="https://wenkokke.github.io/Lists#3171" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[_,_,_,_]</a> <a id="gmail-3181" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3183" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">∀</a> <a id="gmail-3185" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">{</a><a id="gmail-3186" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3188" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3190" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none" moz-do-not-send="true">Set</a><a id="gmail-3193" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">}</a> <a id="gmail-3195" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3197" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3199" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3201" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3203" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3205" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3207" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3209" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3211" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3213" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">List</a> <a id="gmail-3218" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a>
<a id="gmail-3220" href="https://wenkokke.github.io/Lists#3171" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[</a> <a id="gmail-3222" href="https://wenkokke.github.io/Lists#3222" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">w</a> <a id="gmail-3224" href="https://wenkokke.github.io/Lists#3171" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3226" href="https://wenkokke.github.io/Lists#3226" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3228" href="https://wenkokke.github.io/Lists#3171" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3230" href="https://wenkokke.github.io/Lists#3230" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3232" href="https://wenkokke.github.io/Lists#3171" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3234" href="https://wenkokke.github.io/Lists#3234" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3236" href="https://wenkokke.github.io/Lists#3171" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">]</a> <a id="gmail-3238" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">=</a> <a id="gmail-3240" href="https://wenkokke.github.io/Lists#3222" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">w</a> <a id="gmail-3242" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3244" href="https://wenkokke.github.io/Lists#3226" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3246" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3248" href="https://wenkokke.github.io/Lists#3230" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3250" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3252" href="https://wenkokke.github.io/Lists#3234" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3254" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3256" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[]</a>
<a id="gmail-3260" href="https://wenkokke.github.io/Lists#3260" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[_,_,_,_,_]</a> <a id="gmail-3272" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3274" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">∀</a> <a id="gmail-3276" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">{</a><a id="gmail-3277" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3279" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3281" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none" moz-do-not-send="true">Set</a><a id="gmail-3284" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">}</a> <a id="gmail-3286" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3288" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3290" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3292" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3294" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3296" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3298" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3300" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3302" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3304" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3306" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3308" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">List</a> <a id="gmail-3313" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a>
<a id="gmail-3315" href="https://wenkokke.github.io/Lists#3260" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[</a> <a id="gmail-3317" href="https://wenkokke.github.io/Lists#3317" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">v</a> <a id="gmail-3319" href="https://wenkokke.github.io/Lists#3260" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3321" href="https://wenkokke.github.io/Lists#3321" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">w</a> <a id="gmail-3323" href="https://wenkokke.github.io/Lists#3260" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3325" href="https://wenkokke.github.io/Lists#3325" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3327" href="https://wenkokke.github.io/Lists#3260" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3329" href="https://wenkokke.github.io/Lists#3329" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3331" href="https://wenkokke.github.io/Lists#3260" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3333" href="https://wenkokke.github.io/Lists#3333" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3335" href="https://wenkokke.github.io/Lists#3260" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">]</a> <a id="gmail-3337" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">=</a> <a id="gmail-3339" href="https://wenkokke.github.io/Lists#3317" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">v</a> <a id="gmail-3341" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3343" href="https://wenkokke.github.io/Lists#3321" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">w</a> <a id="gmail-3345" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3347" href="https://wenkokke.github.io/Lists#3325" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3349" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3351" href="https://wenkokke.github.io/Lists#3329" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3353" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3355" href="https://wenkokke.github.io/Lists#3333" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3357" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3359" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[]</a>
<a id="gmail-3363" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[_,_,_,_,_,_]</a> <a id="gmail-3377" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3379" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">∀</a> <a id="gmail-3381" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">{</a><a id="gmail-3382" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3384" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">:</a> <a id="gmail-3386" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none" moz-do-not-send="true">Set</a><a id="gmail-3389" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">}</a> <a id="gmail-3391" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3393" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3395" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3397" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3399" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3401" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3403" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3405" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3407" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3409" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3411" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3413" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a> <a id="gmail-3415" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">→</a> <a id="gmail-3417" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">List</a> <a id="gmail-3422" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">A</a>
<a id="gmail-3424" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[</a> <a id="gmail-3426" href="https://wenkokke.github.io/Lists#3426" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">u</a> <a id="gmail-3428" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3430" href="https://wenkokke.github.io/Lists#3430" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">v</a> <a id="gmail-3432" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3434" href="https://wenkokke.github.io/Lists#3434" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">w</a> <a id="gmail-3436" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3438" href="https://wenkokke.github.io/Lists#3438" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3440" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3442" href="https://wenkokke.github.io/Lists#3442" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3444" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">,</a> <a id="gmail-3446" href="https://wenkokke.github.io/Lists#3446" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3448" href="https://wenkokke.github.io/Lists#3363" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">]</a> <a id="gmail-3450" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">=</a> <a id="gmail-3452" href="https://wenkokke.github.io/Lists#3426" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">u</a> <a id="gmail-3454" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3456" href="https://wenkokke.github.io/Lists#3430" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">v</a> <a id="gmail-3458" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3460" href="https://wenkokke.github.io/Lists#3434" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">w</a> <a id="gmail-3462" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3464" href="https://wenkokke.github.io/Lists#3438" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">x</a> <a id="gmail-3466" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3468" href="https://wenkokke.github.io/Lists#3442" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">y</a> <a id="gmail-3470" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3472" href="https://wenkokke.github.io/Lists#3446" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">z</a> <a id="gmail-3474" href="https://wenkokke.github.io/Lists#856" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">∷</a> <a id="gmail-3476" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">[]</a></pre>
This conflicts (in terms of parsing) with the standard
notation for products, so I have altered that slightly:</div>
<div><br>
</div>
<div>
<pre class="gmail-Agda" style="margin:0px 0px 15px;padding:0.4em;font-size:0.85em;border:1px solid rgb(201,225,246);border-radius:3px;background:rgb(232,242,251);overflow-x:auto;font-family:Consolas,Menlo,Monaco,"Lucida Console","Liberation Mono","DejaVu Sans Mono","Bitstream Vera Sans Mono","Courier New",monospace,serif;color:rgb(17,17,17);font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><a id="gmail-638" class="gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none" moz-do-not-send="true">open</a> <a id="gmail-643" class="gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none" moz-do-not-send="true">import</a> <a id="gmail-650" href="https://agda.github.io/agda-stdlib/Data.Product.html" class="gmail-Module" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">Data.Product</a> <a id="gmail-663" class="gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none" moz-do-not-send="true">using</a> <a id="gmail-669" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">(</a><a id="gmail-670" href="https://agda.github.io/agda-stdlib/Data.Product.html#1329" class="gmail-Function gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">_×_</a><a id="gmail-673" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">)</a> <a id="gmail-675" class="gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none" moz-do-not-send="true">renaming</a> <a id="gmail-684" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">(</a><a id="gmail-685" href="https://agda.github.io/agda-stdlib/Data.Product.html#543" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">_,_</a> <a id="gmail-689" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">to</a> <a id="gmail-692" href="https://agda.github.io/agda-stdlib/Data.Product.html#543" class="gmail-InductiveConstructor gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" moz-do-not-send="true">⟨_,_⟩</a><a id="gmail-697" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none" moz-do-not-send="true">)</a></pre>
The question is, have I chosen the best way to deal with the
situation? Or is there an alternative that others recommend?
Cheers, -- P</div>
<div><br>
</div>
<br clear="all">
<div>
<div class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of
Theoretical Computer Science,<br>
. /\ School of Informatics, University of Edinburgh<br>
</div>
<div>. / \ and Senior Research Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a
href="http://homepages.inf.ed.ac.uk/wadler/"
target="_blank" moz-do-not-send="true">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>