<div dir="ltr"><div dir="ltr">On Tue, 1 Feb 2022 at 17:01, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>Hi Eduardo,</div><div><br></div><div>C-c c-n evaluates the given expression in the scope of the current module as it looks like from the outside (i.e. as if you import the module somewhere else). In particular, this scope does not include symbols from modules you have opened, unless they have been opened publicly. So I expect you can solve your problem by adding 'public' to the end of your open statements, e.g. 'open Add "2" public'.</div></div></blockquote><div><br></div><div> Hi Jesper!</div>Ooops and many many thanks!<br>I've added links to your explanation to the right places.<br>For the sake of completeness, here is a demo/test...<br><br>  module NameOfThisFile where<br>  <br>  open import Agda.Builtin.String<br>  open import Agda.Builtin.String.Properties<br>  <br>  infixl 4 _++_<br>  _++_ : String -> String -> String<br>  _++_ str1 str2 = primStringAppend str1 str2<br>  <br>  module Add (i : String) where<br>    infixl 4 _+_<br>    _+_ : String -> String -> String<br>    _+_ a b = "(" ++ a ++ " +_" ++ i ++ " " ++ b ++ ")"<br>  <br>  module Mul (i : String) where<br>    infixl 4 _*_<br>    _*_ : String -> String -> String<br>    _*_ a b = "(" ++ a ++ " *_" ++ i ++ " " ++ b ++ ")"<br>  <br>  module Add0 = Add "0"<br>  module Add1 = Add "1"<br>  open          Add "2" public<br>  open          Mul "3"           -- not "public"<br>  <br>  aa : String<br>  aa = "AAA"<br>  bb : String<br>  bb = "BBB"<br>  cc : String<br>  cc = aa + bb<br>  dd : String<br>  dd = aa * bb<br>  <br>  -- (find-agdanorm "aa ++ bb")<br>  -- (find-agdanorm "Add._+_   \"4\" aa bb")<br>  -- (find-agdanorm "Add0._+_        aa bb")<br>  -- (find-agdanorm "aa Add1.+          bb")<br>  -- (find-agdanorm "aa      +          bb")<br>  -- (find-agdanorm "_+_")<br>  -- (find-agdanorm "_*_")<br>  -- (find-agdanorm "cc")<br>  -- (find-agdanorm "dd")<br>  --<br>  -- Note that find-agdanorm considers that the _*_ is "Not in scope"...<br>  -- See: <a href="https://lists.chalmers.se/pipermail/agda/2022/012862.html">https://lists.chalmers.se/pipermail/agda/2022/012862.html</a><br>  --      <a href="https://lists.chalmers.se/pipermail/agda/2022/012863.html">https://lists.chalmers.se/pipermail/agda/2022/012863.html</a><br><br>Cheers =),<br>  Eduardo Ochs<br>  <a href="http://angg.twu.net/eev-agda.html">http://angg.twu.net/eev-agda.html</a><br></div><div class="gmail_quote"><br></div></div>