<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=""><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures;" class="">Hello,</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures;" class=""><br class=""></span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">when I load the following script, I get a « not in scope ∧ » error.</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Why is that?</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Furthermore, how can I make the <i class="">eq</i> function generic, whichever the types used in the Pair, as long as the first type is equal to the second?</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Many thanks.</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Philippe</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></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: #ed611b" class="">open</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">import</span><span style="font-variant-ligatures: no-common-ligatures" class=""> Agda.Builtin.Nat</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: #ed611b" class="">open</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">import</span><span style="font-variant-ligatures: no-common-ligatures" class=""> Agda.Builtin.String</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: #ed611b" class="">open</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" class="">import</span><span style="font-variant-ligatures: no-common-ligatures" class=""> Agda.Builtin.Bool</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: #ed611b" class="">record</span><span style="font-variant-ligatures: no-common-ligatures" class=""> Pair </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: #4500ff" class="">Set</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #ed611b" 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=""> fst </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=""> snd </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;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">_eq_ </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 </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> Pair Nat Nat</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 </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> Pair Nat Nat</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=""> 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" class="">a eq 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="">Pair.fst a == Pair.fst 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="text-decoration: underline ; font-variant-ligatures: no-common-ligatures; color: #b42419" 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="">Pair.snd a == Pair.snd b</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span></div><div class=""><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class=""><br class=""></span></div></body></html>