<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Philip,<div class=""><br class=""></div><div class="">thank you very much for the pointer. I’ll have a look.</div><div class=""><br class=""></div><div class="">I’m am currently trying to write the two equations, which determine if Pairs A and B match.</div><div class=""><br class=""></div><div class="">Here’s my draft code so far.</div><div class=""><br class=""></div><div class="">Cheers,</div><div class=""><br class=""></div><div class="">Philippe</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(194, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">import</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Relation.Binary.PropositionalEquality</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">using</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">_≡_</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">;</span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">refl</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(237, 97, 27);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">import</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">Data.Bool</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(237, 97, 27);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">import</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">Data.Nat</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">using</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">ℕ</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(237, 97, 27);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">record</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class="">A B </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Set</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Set</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">where</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(237, 97, 27);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">field</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">fst</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> A</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">snd</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> B</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(237, 97, 27);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">open</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">public</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">_eq_</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">{</span><span style="font-variant-ligatures: no-common-ligatures" class="">A B </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Set</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">}</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">((</span><span style="font-variant-ligatures: no-common-ligatures" class="">a a′ </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> A</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Bool</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">((</span><span style="font-variant-ligatures: no-common-ligatures" class="">b b′ </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> B</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Bool</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">ab ab′ </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures" class=""> A B</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Bool</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">eqa </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">eq</span><span style="font-variant-ligatures: no-common-ligatures" class=""> eqb</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">record</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">{</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">fst</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> fst₁ </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">;</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">snd</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> snd₁ </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">}</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">record</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">{</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">fst</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> fst </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">;</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">snd</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> snd </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">}</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> eqb snd snd</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">eqa</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">a a' </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">ℕ</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Bool</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(45, 150, 30);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">eqa</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">ℕ.zero</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> a' </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">false</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">eqa</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">ℕ.suc</span><span style="font-variant-ligatures: no-common-ligatures" class=""> a</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> a' </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">eqa</span><span style="font-variant-ligatures: no-common-ligatures" class=""> a a'</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">eqb</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class="">b b' </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Bool</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Bool</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">eqb</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">false</span><span style="font-variant-ligatures: no-common-ligatures" class=""> b' </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> b'</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">eqb</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">true</span><span style="font-variant-ligatures: no-common-ligatures" class=""> b' </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> b'</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">p23₁</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">ℕ</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Bool</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">p23₁</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">record</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">{</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">fst</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">2</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">;</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">snd</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">true</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">}</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">p23₂</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">ℕ</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Bool</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">p23₂</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">record</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">{</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">fst</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">2</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">;</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">snd</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">true</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">}</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""></span><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">p24</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">ℕ</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">ℕ</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">p24</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">record</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">{</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">fst</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">2</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">;</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #fb198d" class="">snd</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">4</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">}</span></div></div><div class=""><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class=""><br class=""></span></div><div class=""><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class=""><br class=""></span></div><div class=""><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class=""><br class=""></span></div><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">Le 4 mai 2020 à 13:56, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk" class="">wadler@inf.ed.ac.uk</a>> a écrit :</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Philippe,<div class=""><br class=""></div><div class="">You may find the following helpful:</div><div class=""> <a href="https://plfa.github.io/Decidable/" class="">https://plfa.github.io/Decidable/</a></div><div class=""><br class=""></div><div class="">In my experience, you rarely want to use Bool in Agda, and Dec is better instead. The standard library has support for decidable equality on naturals _≟_, and for combining two decidable properties to decide a property of pairs _×-dec_. </div><div class=""><br class=""></div><div class="">Yours, -- P</div><div class=""><br class=""></div><div class=""><div class=""><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr" class=""><div class=""><div dir="ltr" class=""><div dir="ltr" class=""><div class=""><div dir="ltr" class="">. \ Philip Wadler, Professor of Theoretical Computer Science,<br class="">. /\ School of Informatics, University of Edinburgh<br class=""></div><div class="">. / \ and Senior Research Fellow, IOHK<br class=""></div><div dir="ltr" class="">. <span class=""><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank" class="">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr" class=""><br class=""></div></div></div></div></div></div></div><br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 4 May 2020 at 03:01, Philippe de Rochambeau <<a href="mailto:phiroc@free.fr" class="">phiroc@free.fr</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;" class="">Good morning James,<div class=""><br class=""></div><div class="">I spent a few hours yesterday attempting to write the <i class="">fst</i> description procedure, as suggested, but to no avail.</div><div class="">For me, <i class="">fst_desc_proc</i> should compare two values of type <i class="">A</i> and, if they are equal, return <i class="">true</i>, otherwise, <i class="">false</i>.</div><div class="">But how how do you generically compare two A values? ≡ won’t do.</div><div class=""><br class=""></div><div class="">(In fact, I wouldn’t know either how to compare two <i class="">Nats</i> for equality in Agda, since I could not find an <i class="">==</i> operator in <i class="">Data.Nats</i>).</div><div class=""><br class=""></div><div class="">Cheers,</div><div class=""><br class=""></div><div class="">Philippe</div><div class=""><div class=""><br class=""></div><div class=""><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">open</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">import</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(194,0,255)" class="">Data.Nat</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">using</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">(</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)" class="">ℕ</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">)</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(194,0,255)" class=""><span style="font-variant-ligatures:no-common-ligatures;color:rgb(237,97,27)" class="">open</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(237,97,27)" class="">import</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">Relation.Binary.PropositionalEquality</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(237,97,27)" class="">using</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">(</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)" class="">_≡_</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">)</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">open</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">import</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(194,0,255)" class="">Data.Bool</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px" class=""><br class=""><span style="font-variant-ligatures:no-common-ligatures" class=""></span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">record</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">(</span><span style="font-variant-ligatures: no-common-ligatures;" class="">A B </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">:</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)" class="">Set</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">)</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">:</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)" class="">Set</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">where</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)" class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">field</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(251,25,141)" class="">fst</span><span style="font-variant-ligatures:no-common-ligatures" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">:</span><span style="font-variant-ligatures:no-common-ligatures" class=""> A</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(251,25,141)" class="">snd</span><span style="font-variant-ligatures:no-common-ligatures" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">:</span><span style="font-variant-ligatures:no-common-ligatures" class=""> B</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""></span><br class=""></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">open</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(194,0,255)" class="">Pair</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">public</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""></span><br class=""></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">{-- </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">_eq_ : {A B : Set} → (a : Pair A B) → (b : Pair A B) → Bool </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">a eq b = (fst a ≡ fst b) ∧ (snd a ≡ snd b) </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">--}</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""></span><br class=""></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(69,0,255)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">fst_desc_proc</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">:</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">{</span><span style="font-variant-ligatures: no-common-ligatures;" class="">A </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">:</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">Set</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">}</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">→</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">(</span><span style="font-variant-ligatures: no-common-ligatures;" class="">a a' </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">:</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> A</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">)</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">→</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures" class="">Bool</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(69,0,255)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">fst_desc_proc</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> a a' </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">=</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="text-decoration:underline;font-variant-ligatures:no-common-ligatures;color:rgb(180,36,25)" class="">a</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="text-decoration:underline;font-variant-ligatures:no-common-ligatures;color:rgb(180,36,25)" class="">≡</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="text-decoration:underline;font-variant-ligatures:no-common-ligatures;color:rgb(180,36,25)" class="">a'</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(69,0,255)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">fst_desc_proc</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">=</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)" class="">{!!}</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px" class=""><span style="font-variant-ligatures:no-common-ligatures" class=""></span><br class=""></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">{-- </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">snd_desc_proc : {B : Set} → (b b' : B) → Bool </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">snd_desc_proc b b' = b == b' → true </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">snd_desc_proc b b' = b != b' → false </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">--}</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">-- _eq_ : {A B : Set} → ((a a′ : A) → Bool) → ((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)" class=""><span style="font-variant-ligatures:no-common-ligatures" class="">-- a eq a' = ?</span></div><div class=""><span style="font-variant-ligatures:no-common-ligatures" class=""><br class=""></span></div><div class=""><br class=""></div><div class=""><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">Le 3 mai 2020 à 19:56, James Wood <<a href="mailto:james.wood.100@strath.ac.uk" target="_blank" class="">james.wood.100@strath.ac.uk</a>> a écrit :</div><br class=""><div class=""><div class="">Hi Philippe,<br class=""><br class="">You can see from the source code of `Agda.Builtin.Bool` that it defines<br class="">only `Bool`, `true`, and `false`. If you want some operations on<br class="">Booleans, you can either define them yourself or get them from a<br class="">library, e.g, stdlib's `Data.Bool`. It's best practice to not import<br class="">`Agda.Builtin` modules unless you really have to (e.g, if you are<br class="">writing your own base library). They may change between versions.<br class=""><br class="">For making your `eq` generic, the simplest thing to do would be to take<br class="">as arguments decision procedures for the `fst`s and `snd`s,<br class="">respectively. The type should be `{A B : Set} → ((a a′ : A) → Bool) →<br class="">((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool`.<br class=""><br class="">Additionally, you might want to add `open Pair public` after your<br class="">definition of `Pair`, so that you don't have to qualify `fst` and `snd`.<br class="">There's an example of this in stdlib's definition of `Σ` (somewhere<br class="">around `Data.Product`).<br class=""><br class="">Regards,<br class="">James<br class=""><br class="">On 03/05/2020 17:50, Philippe de Rochambeau wrote:<br class=""><blockquote type="cite" class="">Hello,<br class=""><br class="">when I load the following script, I get a « not in scope ∧ » error.<br class="">Why is that?<br class="">Furthermore, how can I make the /eq/ function generic, whichever the<br class="">types used in the Pair, as long as the first type is equal to the second?<br class="">Many thanks.<br class="">Philippe<br class=""><br class=""><br class="">openimportAgda.Builtin.Nat<br class="">openimportAgda.Builtin.String<br class="">openimportAgda.Builtin.Bool<br class=""><br class="">recordPair (A B :Set):Setwhere<br class=""> field<br class=""> fst :A<br class=""> snd :B<br class=""><br class="">_eq_ :(a :Pair Nat Nat)→(b :Pair Nat Nat)→Bool<br class="">a eq b =(Pair.fst a == Pair.fst b)∧(Pair.snd a == Pair.snd b)<br class=""><br class=""><br class="">_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class=""><br class=""></blockquote>_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class=""><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class=""></div></div></blockquote></div><br class=""></div></div></div></div>_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</blockquote></div>
The University of Edinburgh is a charitable body, registered in<br class="">Scotland, with registration number SC005336.<br class=""></div></blockquote></div><br class=""></div></body></html>