<div dir="ltr">Guillaume,<div><br></div><div>Thank you for the suggestion. I tried something similar, but gave it up because I wanted to write</div><div><br></div><div> map (1 +_) [ 0 , 1 , 2 ]</div><div><br></div><div>rather than</div><div><br></div><div> map (1 +_) ([ 0 , 1 , 2 ])</div><div><br></div><div>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.</div><div><br></div><div>Cheers, -- P</div></div><div class="gmail_extra"><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>
<br><div class="gmail_quote">On 2 March 2018 at 12:51, Guillaume Allais <span dir="ltr"><<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div 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>==============================<wbr>===================<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>
==============================<wbr>===================<br>
</tt><div><div class="h5"><br>
<div class="m_3409482949069775611moz-cite-prefix">On 02/03/18 12:40, Philip Wadler wrote:<br>
</div>
</div></div><blockquote type="cite"><div><div class="h5">
<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="m_3409482949069775611gmail-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="m_3409482949069775611gmail-2988" href="https://wenkokke.github.io/Lists#2988" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[_]</a> <a id="m_3409482949069775611gmail-2992" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-2994" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="m_3409482949069775611gmail-2996" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="m_3409482949069775611gmail-2997" href="https://wenkokke.github.io/Lists#2997" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-2999" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3001" class="m_3409482949069775611gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="m_3409482949069775611gmail-3004" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="m_3409482949069775611gmail-3006" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3008" href="https://wenkokke.github.io/Lists#2997" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3010" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3012" href="https://wenkokke.github.io/Lists#813" class="m_3409482949069775611gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" target="_blank">List</a> <a id="m_3409482949069775611gmail-3017" href="https://wenkokke.github.io/Lists#2997" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a>
<a id="m_3409482949069775611gmail-3019" href="https://wenkokke.github.io/Lists#2988" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[</a> <a id="m_3409482949069775611gmail-3021" href="https://wenkokke.github.io/Lists#3021" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3023" href="https://wenkokke.github.io/Lists#2988" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">]</a> <a id="m_3409482949069775611gmail-3025" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="m_3409482949069775611gmail-3027" href="https://wenkokke.github.io/Lists#3021" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3029" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3031" href="https://wenkokke.github.io/Lists#842" class="m_3409482949069775611gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[]</a>
<a id="m_3409482949069775611gmail-3035" href="https://wenkokke.github.io/Lists#3035" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[_,_]</a> <a id="m_3409482949069775611gmail-3041" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3043" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="m_3409482949069775611gmail-3045" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="m_3409482949069775611gmail-3046" href="https://wenkokke.github.io/Lists#3046" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3048" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3050" class="m_3409482949069775611gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="m_3409482949069775611gmail-3053" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="m_3409482949069775611gmail-3055" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3057" href="https://wenkokke.github.io/Lists#3046" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3059" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3061" href="https://wenkokke.github.io/Lists#3046" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3063" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3065" href="https://wenkokke.github.io/Lists#813" class="m_3409482949069775611gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" target="_blank">List</a> <a id="m_3409482949069775611gmail-3070" href="https://wenkokke.github.io/Lists#3046" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a>
<a id="m_3409482949069775611gmail-3072" href="https://wenkokke.github.io/Lists#3035" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[</a> <a id="m_3409482949069775611gmail-3074" href="https://wenkokke.github.io/Lists#3074" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3076" href="https://wenkokke.github.io/Lists#3035" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3078" href="https://wenkokke.github.io/Lists#3078" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3080" href="https://wenkokke.github.io/Lists#3035" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">]</a> <a id="m_3409482949069775611gmail-3082" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="m_3409482949069775611gmail-3084" href="https://wenkokke.github.io/Lists#3074" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3086" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3088" href="https://wenkokke.github.io/Lists#3078" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3090" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3092" href="https://wenkokke.github.io/Lists#842" class="m_3409482949069775611gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[]</a>
<a id="m_3409482949069775611gmail-3096" href="https://wenkokke.github.io/Lists#3096" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[_,_,_]</a> <a id="m_3409482949069775611gmail-3104" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3106" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="m_3409482949069775611gmail-3108" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="m_3409482949069775611gmail-3109" href="https://wenkokke.github.io/Lists#3109" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3111" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3113" class="m_3409482949069775611gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="m_3409482949069775611gmail-3116" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="m_3409482949069775611gmail-3118" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3120" href="https://wenkokke.github.io/Lists#3109" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3122" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3124" href="https://wenkokke.github.io/Lists#3109" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3126" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3128" href="https://wenkokke.github.io/Lists#3109" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3130" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3132" href="https://wenkokke.github.io/Lists#813" class="m_3409482949069775611gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" target="_blank">List</a> <a id="m_3409482949069775611gmail-3137" href="https://wenkokke.github.io/Lists#3109" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a>
<a id="m_3409482949069775611gmail-3139" href="https://wenkokke.github.io/Lists#3096" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[</a> <a id="m_3409482949069775611gmail-3141" href="https://wenkokke.github.io/Lists#3141" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3143" href="https://wenkokke.github.io/Lists#3096" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3145" href="https://wenkokke.github.io/Lists#3145" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3147" href="https://wenkokke.github.io/Lists#3096" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3149" href="https://wenkokke.github.io/Lists#3149" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3151" href="https://wenkokke.github.io/Lists#3096" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">]</a> <a id="m_3409482949069775611gmail-3153" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="m_3409482949069775611gmail-3155" href="https://wenkokke.github.io/Lists#3141" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3157" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3159" href="https://wenkokke.github.io/Lists#3145" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3161" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3163" href="https://wenkokke.github.io/Lists#3149" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3165" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3167" href="https://wenkokke.github.io/Lists#842" class="m_3409482949069775611gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[]</a>
<a id="m_3409482949069775611gmail-3171" href="https://wenkokke.github.io/Lists#3171" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[_,_,_,_]</a> <a id="m_3409482949069775611gmail-3181" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3183" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="m_3409482949069775611gmail-3185" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="m_3409482949069775611gmail-3186" href="https://wenkokke.github.io/Lists#3186" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3188" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3190" class="m_3409482949069775611gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="m_3409482949069775611gmail-3193" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="m_3409482949069775611gmail-3195" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3197" href="https://wenkokke.github.io/Lists#3186" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3199" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3201" href="https://wenkokke.github.io/Lists#3186" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3203" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3205" href="https://wenkokke.github.io/Lists#3186" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3207" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3209" href="https://wenkokke.github.io/Lists#3186" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3211" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3213" href="https://wenkokke.github.io/Lists#813" class="m_3409482949069775611gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" target="_blank">List</a> <a id="m_3409482949069775611gmail-3218" href="https://wenkokke.github.io/Lists#3186" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a>
<a id="m_3409482949069775611gmail-3220" href="https://wenkokke.github.io/Lists#3171" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[</a> <a id="m_3409482949069775611gmail-3222" href="https://wenkokke.github.io/Lists#3222" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">w</a> <a id="m_3409482949069775611gmail-3224" href="https://wenkokke.github.io/Lists#3171" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3226" href="https://wenkokke.github.io/Lists#3226" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3228" href="https://wenkokke.github.io/Lists#3171" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3230" href="https://wenkokke.github.io/Lists#3230" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3232" href="https://wenkokke.github.io/Lists#3171" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3234" href="https://wenkokke.github.io/Lists#3234" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3236" href="https://wenkokke.github.io/Lists#3171" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">]</a> <a id="m_3409482949069775611gmail-3238" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="m_3409482949069775611gmail-3240" href="https://wenkokke.github.io/Lists#3222" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">w</a> <a id="m_3409482949069775611gmail-3242" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3244" href="https://wenkokke.github.io/Lists#3226" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3246" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3248" href="https://wenkokke.github.io/Lists#3230" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3250" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3252" href="https://wenkokke.github.io/Lists#3234" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3254" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3256" href="https://wenkokke.github.io/Lists#842" class="m_3409482949069775611gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[]</a>
<a id="m_3409482949069775611gmail-3260" href="https://wenkokke.github.io/Lists#3260" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[_,_,_,_,_]</a> <a id="m_3409482949069775611gmail-3272" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3274" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="m_3409482949069775611gmail-3276" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="m_3409482949069775611gmail-3277" href="https://wenkokke.github.io/Lists#3277" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3279" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3281" class="m_3409482949069775611gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="m_3409482949069775611gmail-3284" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="m_3409482949069775611gmail-3286" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3288" href="https://wenkokke.github.io/Lists#3277" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3290" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3292" href="https://wenkokke.github.io/Lists#3277" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3294" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3296" href="https://wenkokke.github.io/Lists#3277" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3298" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3300" href="https://wenkokke.github.io/Lists#3277" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3302" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3304" href="https://wenkokke.github.io/Lists#3277" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3306" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3308" href="https://wenkokke.github.io/Lists#813" class="m_3409482949069775611gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" target="_blank">List</a> <a id="m_3409482949069775611gmail-3313" href="https://wenkokke.github.io/Lists#3277" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a>
<a id="m_3409482949069775611gmail-3315" href="https://wenkokke.github.io/Lists#3260" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[</a> <a id="m_3409482949069775611gmail-3317" href="https://wenkokke.github.io/Lists#3317" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">v</a> <a id="m_3409482949069775611gmail-3319" href="https://wenkokke.github.io/Lists#3260" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3321" href="https://wenkokke.github.io/Lists#3321" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">w</a> <a id="m_3409482949069775611gmail-3323" href="https://wenkokke.github.io/Lists#3260" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3325" href="https://wenkokke.github.io/Lists#3325" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3327" href="https://wenkokke.github.io/Lists#3260" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3329" href="https://wenkokke.github.io/Lists#3329" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3331" href="https://wenkokke.github.io/Lists#3260" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3333" href="https://wenkokke.github.io/Lists#3333" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3335" href="https://wenkokke.github.io/Lists#3260" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">]</a> <a id="m_3409482949069775611gmail-3337" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="m_3409482949069775611gmail-3339" href="https://wenkokke.github.io/Lists#3317" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">v</a> <a id="m_3409482949069775611gmail-3341" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3343" href="https://wenkokke.github.io/Lists#3321" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">w</a> <a id="m_3409482949069775611gmail-3345" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3347" href="https://wenkokke.github.io/Lists#3325" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3349" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3351" href="https://wenkokke.github.io/Lists#3329" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3353" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3355" href="https://wenkokke.github.io/Lists#3333" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3357" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3359" href="https://wenkokke.github.io/Lists#842" class="m_3409482949069775611gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[]</a>
<a id="m_3409482949069775611gmail-3363" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[_,_,_,_,_,_]</a> <a id="m_3409482949069775611gmail-3377" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3379" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">∀</a> <a id="m_3409482949069775611gmail-3381" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">{</a><a id="m_3409482949069775611gmail-3382" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3384" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">:</a> <a id="m_3409482949069775611gmail-3386" class="m_3409482949069775611gmail-PrimitiveType" style="color:rgb(0,0,205);text-decoration:none">Set</a><a id="m_3409482949069775611gmail-3389" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">}</a> <a id="m_3409482949069775611gmail-3391" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3393" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3395" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3397" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3399" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3401" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3403" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3405" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3407" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3409" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3411" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3413" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a> <a id="m_3409482949069775611gmail-3415" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">→</a> <a id="m_3409482949069775611gmail-3417" href="https://wenkokke.github.io/Lists#813" class="m_3409482949069775611gmail-Datatype" style="color:rgb(23,86,169);text-decoration:none" target="_blank">List</a> <a id="m_3409482949069775611gmail-3422" href="https://wenkokke.github.io/Lists#3382" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">A</a>
<a id="m_3409482949069775611gmail-3424" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[</a> <a id="m_3409482949069775611gmail-3426" href="https://wenkokke.github.io/Lists#3426" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">u</a> <a id="m_3409482949069775611gmail-3428" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3430" href="https://wenkokke.github.io/Lists#3430" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">v</a> <a id="m_3409482949069775611gmail-3432" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3434" href="https://wenkokke.github.io/Lists#3434" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">w</a> <a id="m_3409482949069775611gmail-3436" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3438" href="https://wenkokke.github.io/Lists#3438" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3440" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3442" href="https://wenkokke.github.io/Lists#3442" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3444" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">,</a> <a id="m_3409482949069775611gmail-3446" href="https://wenkokke.github.io/Lists#3446" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3448" href="https://wenkokke.github.io/Lists#3363" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">]</a> <a id="m_3409482949069775611gmail-3450" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">=</a> <a id="m_3409482949069775611gmail-3452" href="https://wenkokke.github.io/Lists#3426" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">u</a> <a id="m_3409482949069775611gmail-3454" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3456" href="https://wenkokke.github.io/Lists#3430" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">v</a> <a id="m_3409482949069775611gmail-3458" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3460" href="https://wenkokke.github.io/Lists#3434" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">w</a> <a id="m_3409482949069775611gmail-3462" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3464" href="https://wenkokke.github.io/Lists#3438" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">x</a> <a id="m_3409482949069775611gmail-3466" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3468" href="https://wenkokke.github.io/Lists#3442" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">y</a> <a id="m_3409482949069775611gmail-3470" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3472" href="https://wenkokke.github.io/Lists#3446" class="m_3409482949069775611gmail-Bound" style="color:rgb(23,86,169);text-decoration:none" target="_blank">z</a> <a id="m_3409482949069775611gmail-3474" href="https://wenkokke.github.io/Lists#856" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">∷</a> <a id="m_3409482949069775611gmail-3476" href="https://wenkokke.github.io/Lists#842" class="m_3409482949069775611gmail-InductiveConstructor" style="color:rgb(23,86,169);text-decoration:none" target="_blank">[]</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="m_3409482949069775611gmail-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="m_3409482949069775611gmail-638" class="m_3409482949069775611gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none">open</a> <a id="m_3409482949069775611gmail-643" class="m_3409482949069775611gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none">import</a> <a id="m_3409482949069775611gmail-650" href="https://agda.github.io/agda-stdlib/Data.Product.html" class="m_3409482949069775611gmail-Module" style="color:rgb(23,86,169);text-decoration:none" target="_blank">Data.Product</a> <a id="m_3409482949069775611gmail-663" class="m_3409482949069775611gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none">using</a> <a id="m_3409482949069775611gmail-669" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">(</a><a id="m_3409482949069775611gmail-670" href="https://agda.github.io/agda-stdlib/Data.Product.html#1329" class="m_3409482949069775611gmail-Function m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">_×_</a><a id="m_3409482949069775611gmail-673" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">)</a> <a id="m_3409482949069775611gmail-675" class="m_3409482949069775611gmail-Keyword" style="color:rgb(205,102,0);text-decoration:none">renaming</a> <a id="m_3409482949069775611gmail-684" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">(</a><a id="m_3409482949069775611gmail-685" href="https://agda.github.io/agda-stdlib/Data.Product.html#543" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">_,_</a> <a id="m_3409482949069775611gmail-689" class="m_3409482949069775611gmail-Symbol" style="color:rgb(64,64,64);text-decoration:none">to</a> <a id="m_3409482949069775611gmail-692" href="https://agda.github.io/agda-stdlib/Data.Product.html#543" class="m_3409482949069775611gmail-InductiveConstructor m_3409482949069775611gmail-Operator" style="color:rgb(23,86,169);text-decoration:none" target="_blank">⟨_,_⟩</a><a id="m_3409482949069775611gmail-697" class="m_3409482949069775611gmail-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="m_3409482949069775611gmail_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/<wbr>wadler/</a></span></div>
</div>
</div>
</div>
</div>
</div>
<br>
<fieldset class="m_3409482949069775611mimeAttachmentHeader"></fieldset>
<br>
</div></div><pre>The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
</pre>
<br>
<fieldset class="m_3409482949069775611mimeAttachmentHeader"></fieldset>
<br>
<pre>______________________________<wbr>_________________
Agda mailing list
<a class="m_3409482949069775611moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a class="m_3409482949069775611moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>