<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 all,<div class="">thank you for your suggestions.</div><div class="">I am currently reading through the book entitled <i class="">The Little Typer.</i></div><div class="">On p. 17, the authors mention <i class="">Pairs, </i><span style="font-style: normal;" class="">which</span><i class=""> </i><span style="font-style: normal;" class="">I tried to convert to Agda:</span></div><div class=""><div class=""><br class=""></div><div class=""><i class="">… the normal form of</i></div><div class=""><i class="">(Pair</i></div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>(car </i></div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>(cons Atom ‘olive))</i></div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>(cdr</i></div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>(cons ‘oil Atom)))</i></div><div class=""><i class=""><br class=""></i></div><div class=""><i class="">is </i></div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>(Pair Atom Atom),</i></div><div class=""><i class="">and</i></div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>(cons ‘ratatouille ‘baguette)</i></div><div class=""><i class="">is a</i></div><div class=""><i class=""><span class="Apple-tab-span" style="white-space:pre"> </span>(Pair Atom Atom).</i></div><div class=""><br class=""><div class=""><div class="">Apparently, Pair is a <i class="">type constructor</i> (cf. TLT, p. 30) and is closely associated with what they call <i class="">The Normal Form.</i></div><div class=""><br class=""></div><div class="">« Given a type, every expression described by that type has a normal form, which is the most direct way of writing it » , p. 13</div><div class=""><br class=""></div><div class="">Philippe</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""><div><blockquote type="cite" class=""><div class="">Le 3 mai 2020 à 20:00, <a href="mailto:mechvel@scico.botik.ru" class="">mechvel@scico.botik.ru</a> a écrit :</div><br class="Apple-interchange-newline"><div class=""><div class="">On 2020-05-03 19:50, Philippe de Rochambeau wrote:<br class=""><blockquote type="cite" class="">Hello,<br class="">when I load the following script, I get a « not in scope ∧ »<br class="">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<br class="">second?<br class="">Many thanks.<br class="">Philippe<br class="">open import Agda.Builtin.Nat<br class="">open import Agda.Builtin.String<br class="">open import Agda.Builtin.Bool<br class="">record Pair (A B : Set) : Set where<br class=""> field<br class=""> fst : A<br class=""> snd : B<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=""></blockquote><br class=""><br class="">If you add<br class=""><br class="">open import Data.Bool using (_∧_)<br class=""><br class="">then it is type-checked.<br class="">But I never used "Agda.Builtin" explicitly, and do not know what is the goal.<br class=""><br class="">Regards,<br class=""><br class="">------<br class="">Sergei<br class=""><br class=""></div></div></blockquote></div><br class=""></div></div></div></div></body></html>