<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="">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; 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; 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></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; 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; 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; 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; 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="">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="">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: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class="">a 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=""> 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; 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; 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; color: #000000" class=""> a 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="text-decoration: underline ; font-variant-ligatures: no-common-ligatures; color: #b42419" class="">a</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="text-decoration: underline ; font-variant-ligatures: no-common-ligatures; color: #b42419" class="">≡</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="text-decoration: underline ; font-variant-ligatures: no-common-ligatures; color: #b42419" 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; 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></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><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" class="">james.wood.100@strath.ac.uk</a>> a écrit :</div><br class="Apple-interchange-newline"><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" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""><br class=""></blockquote>_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></div></blockquote></div><br class=""></div></div></div></body></html>