<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">[_]</a> <a id="gmail-2992" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-2994" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="gmail-2996" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="gmail-2997" href="https://wenkokke.github.io/Lists#2997" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-2999" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3001" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="gmail-3004" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="gmail-3006" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3008" href="https://wenkokke.github.io/Lists#2997" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3010" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3012" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none">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">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">[</a> <a id="gmail-3021" href="https://wenkokke.github.io/Lists#3021" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">]</a> <a id="gmail-3025" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="gmail-3027" href="https://wenkokke.github.io/Lists#3021" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3031" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none">[]</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">[_,_]</a> <a id="gmail-3041" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3043" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="gmail-3045" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="gmail-3046" href="https://wenkokke.github.io/Lists#3046" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3048" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3050" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="gmail-3053" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="gmail-3055" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3057" href="https://wenkokke.github.io/Lists#3046" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3059" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3061" href="https://wenkokke.github.io/Lists#3046" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3063" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3065" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none">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">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">[</a> <a id="gmail-3074" href="https://wenkokke.github.io/Lists#3074" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3078" href="https://wenkokke.github.io/Lists#3078" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">]</a> <a id="gmail-3082" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="gmail-3084" href="https://wenkokke.github.io/Lists#3074" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3088" href="https://wenkokke.github.io/Lists#3078" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3092" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none">[]</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">[_,_,_]</a> <a id="gmail-3104" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3106" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="gmail-3108" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="gmail-3109" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3111" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3113" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="gmail-3116" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="gmail-3118" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3120" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3122" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3124" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3126" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3128" href="https://wenkokke.github.io/Lists#3109" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3130" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3132" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none">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">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">[</a> <a id="gmail-3141" href="https://wenkokke.github.io/Lists#3141" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3145" href="https://wenkokke.github.io/Lists#3145" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3149" href="https://wenkokke.github.io/Lists#3149" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">]</a> <a id="gmail-3153" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="gmail-3155" href="https://wenkokke.github.io/Lists#3141" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3159" href="https://wenkokke.github.io/Lists#3145" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3163" href="https://wenkokke.github.io/Lists#3149" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3167" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none">[]</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">[_,_,_,_]</a> <a id="gmail-3181" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3183" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="gmail-3185" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="gmail-3186" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3188" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3190" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="gmail-3193" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="gmail-3195" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3197" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3199" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3201" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3203" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3205" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3207" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3209" href="https://wenkokke.github.io/Lists#3186" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3211" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3213" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none">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">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">[</a> <a id="gmail-3222" href="https://wenkokke.github.io/Lists#3222" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3226" href="https://wenkokke.github.io/Lists#3226" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3230" href="https://wenkokke.github.io/Lists#3230" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3234" href="https://wenkokke.github.io/Lists#3234" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">]</a> <a id="gmail-3238" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="gmail-3240" href="https://wenkokke.github.io/Lists#3222" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3244" href="https://wenkokke.github.io/Lists#3226" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3248" href="https://wenkokke.github.io/Lists#3230" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3252" href="https://wenkokke.github.io/Lists#3234" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3256" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none">[]</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">[_,_,_,_,_]</a> <a id="gmail-3272" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3274" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="gmail-3276" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="gmail-3277" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3279" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3281" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="gmail-3284" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="gmail-3286" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3288" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3290" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3292" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3294" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3296" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3298" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3300" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3302" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3304" href="https://wenkokke.github.io/Lists#3277" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3306" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3308" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none">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">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">[</a> <a id="gmail-3317" href="https://wenkokke.github.io/Lists#3317" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3321" href="https://wenkokke.github.io/Lists#3321" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3325" href="https://wenkokke.github.io/Lists#3325" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3329" href="https://wenkokke.github.io/Lists#3329" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3333" href="https://wenkokke.github.io/Lists#3333" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">]</a> <a id="gmail-3337" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="gmail-3339" href="https://wenkokke.github.io/Lists#3317" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3343" href="https://wenkokke.github.io/Lists#3321" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3347" href="https://wenkokke.github.io/Lists#3325" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3351" href="https://wenkokke.github.io/Lists#3329" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3355" href="https://wenkokke.github.io/Lists#3333" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3359" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none">[]</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">[_,_,_,_,_,_]</a> <a id="gmail-3377" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3379" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="gmail-3381" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="gmail-3382" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3384" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="gmail-3386" class="gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="gmail-3389" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="gmail-3391" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3393" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3395" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3397" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3399" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3401" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3403" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3405" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3407" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3409" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3411" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3413" href="https://wenkokke.github.io/Lists#3382" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">A</a> <a id="gmail-3415" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="gmail-3417" href="https://wenkokke.github.io/Lists#813" class="gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none">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">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">[</a> <a id="gmail-3426" href="https://wenkokke.github.io/Lists#3426" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3430" href="https://wenkokke.github.io/Lists#3430" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3434" href="https://wenkokke.github.io/Lists#3434" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3438" href="https://wenkokke.github.io/Lists#3438" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3442" href="https://wenkokke.github.io/Lists#3442" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">,</a> <a id="gmail-3446" href="https://wenkokke.github.io/Lists#3446" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">]</a> <a id="gmail-3450" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="gmail-3452" href="https://wenkokke.github.io/Lists#3426" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3456" href="https://wenkokke.github.io/Lists#3430" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3460" href="https://wenkokke.github.io/Lists#3434" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3464" href="https://wenkokke.github.io/Lists#3438" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3468" href="https://wenkokke.github.io/Lists#3442" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3472" href="https://wenkokke.github.io/Lists#3446" class="gmail-Bound" style="color:rgb(23,86,169);text-decoration:none">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">∷</a> <a id="gmail-3476" href="https://wenkokke.github.io/Lists#842" class="gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none">[]</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">open</a> <a id="gmail-643" class="gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none">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">Data.Product</a> <a id="gmail-663" class="gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none">using</a> <a id="gmail-669" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">(</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">_×_</a><a id="gmail-673" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">)</a> <a id="gmail-675" class="gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none">renaming</a> <a id="gmail-684" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">(</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">_,_</a> <a id="gmail-689" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">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">⟨_,_⟩</a><a id="gmail-697" class="gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">)</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">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div>