<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 Alex,<div class="">commenting out <font color="#c200ff" face="Menlo" class="">Eq.≡-Reasoning</font><font face="Menlo" class="">’s <i class="">using</i> statement</font><span style="caret-color: rgb(194, 0, 255); font-family: Menlo;" class=""> worked.</span></div><div class=""><span style="caret-color: rgb(194, 0, 255);" class="">Many thanks.</span></div><div class=""><span style="caret-color: rgb(194, 0, 255);" class="">Pleasant evening.</span></div><div class=""><span style="caret-color: rgb(194, 0, 255);" class="">Philippe</span></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="">module</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #c200ff" class="">Induct</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; 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(194, 0, 255);" class=""><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: #535353" class="">as</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">Eq</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; 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: #c200ff" class="">Eq</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" 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: #2d961e" class="">refl</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="">cong</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="">sym</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(203, 36, 24);" 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: #c200ff" class="">Eq.≡-Reasoning</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">-- using (begin_; _≡⟨⟩_; _∎)</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><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">zero</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: #2d961e" class="">suc</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="">_+_</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="">_*_</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="">_∸_</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;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+-assoc</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=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">m n p </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: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">m </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> n</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" class=""> p </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">≡</span><span style="font-variant-ligatures: no-common-ligatures" class=""> m </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" 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="">n </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> p</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(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">+-assoc</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">zero</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> n p </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(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">begin</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: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">zero</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" class=""> n</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" class=""> p</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; 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" class=""> n </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> p</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; 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" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">zero</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" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">n </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> p</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;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" 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;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+-assoc</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=""> m</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> n p </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(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures" class="">begin</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: #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=""> m </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> n</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" class=""> p</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; 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" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">suc</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="">m </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> n</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" class=""> p</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; 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" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">suc</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="">m </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> n</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" class=""> p</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(69, 0, 255);" class=""><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="">cong</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">suc</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" class="">+-assoc</span><span style="font-variant-ligatures: no-common-ligatures; color: #000000" class=""> m n p</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="">⟩</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: #2d961e" class="">suc</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="">m </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" 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="">n </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> p</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(69, 0, 255);" class=""><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" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #2d961e" class="">suc</span><span style="font-variant-ligatures: no-common-ligatures" class=""> m </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" 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="">n </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">+</span><span style="font-variant-ligatures: no-common-ligatures" class=""> p</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;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" 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; min-height: 21px;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; min-height: 21px;" class=""><br class=""></div><div><br class=""><blockquote type="cite" class=""><div class="">Le 4 mai 2020 à 18:47, Alexander Ben Nasrallah <<a href="mailto:me@abn.sh" class="">me@abn.sh</a>> a écrit :</div><br class="Apple-interchange-newline"><div class=""><div class="">Hi Philippe,<br class=""><br class="">On Mon, May 04, 2020 at 06:27:58PM +0200, Philippe de Rochambeau wrote:<br class=""><blockquote type="cite" class="">The <a href="https://plfa.github.io/Induction" class="">https://plfa.github.io/Induction</a> Page mentions the _≡⟨_⟩_<br class="">operator, which I couldn’t find on<br class=""><a href="https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.Core.html" class="">https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.Core.html</a><br class=""></blockquote><br class=""><blockquote type="cite" class="">Does it have an existing equivalent in the Standard Library?<br class=""></blockquote><br class="">You have to be careful about the stdlib version. plfa uses v1.2.<br class="">The current version is v1.3.<br class=""><br class="">Assuming you installed Agda stdlib v1.3, did you try?<br class=""><br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>import Relation.Binary.PropositionalEquality as Eq<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>open Eq using (_≡_; refl; cong; sym)<br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>open Eq.≡-Reasoning<br class=""><br class="">Note the missing using statement compared to the code in plfa. With<br class="">stdlib v1.3 you can’t use `using` or `hide` with _≡⟨⟩_. They changed the<br class="">definition<br class=""><a href="https://github.com/agda/agda-stdlib/blob/v1.3/CHANGELOG.md#changes-to-how-equational-reasoning-is-implemented" class="">https://github.com/agda/agda-stdlib/blob/v1.3/CHANGELOG.md#changes-to-how-equational-reasoning-is-implemented</a><br class=""><br class="">I don’t unterstand the details why it doesn’t work anymore, I just know<br class="">how to deal with it ^^<br class=""><br class="">Hope that helps.<br class="">Alex<br class=""><br class="">_______________________________________________<br class="">Agda mailing list<br class="">Agda@lists.chalmers.se<br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></div></blockquote></div><br class=""></div></div></body></html>