<div dir="ltr">Hello list,<br><br>I think that I found a quirk on the behavior of `C-c C-n'. When I was<br>trying to write a minimal example that showed the problem I wrote<br>this, that isn't really minimal but that should be minimal enough...<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>    add   : String -> String -> String<br>    add   a b = "(" ++ a ++ " +_" ++ i ++ " " ++ b ++ ")"<br>    _+++_ : String -> String -> String<br>    _+++_ a b = add a b<br>  <br>  module Add0 = Add "0"<br>  module Add1 = Add "1"<br>  -- open Add0<br>  open          Add "2"<br>  <br>  aa : String<br>  aa = "AAA"<br>  bb : String<br>  bb = "BBB"<br>  cc : String<br>  cc = aa +++ bb<br>  <br>  -- (find-agdanorm "aa ++ bb")<br>  -- (find-agdanorm "Add.add   \"4\" aa bb")<br>  -- (find-agdanorm "Add0.add        aa bb")<br>  -- (find-agdanorm "Add._+++_ \"9\" aa bb")<br>  -- (find-agdanorm "Add0._+++_      aa bb")<br>  -- (find-agdanorm "aa Add0.+++ bb")<br>  -- (find-agdanorm "aa +++ bb")<br>  -- (find-agdanorm "_+++_")<br>  -- (find-agdatype "_+++_")<br>  -- (find-agdanorm "cc")<br><br>The sexps like (find-agdanorm "<expr>") in comments use a hack that I<br>wrote that is simple to explain. The docstring of find-agdanorm is:<br><br>  (find-agdanorm AGDAEXPR &rest REST)<br><br>  Show the normalized value  of AGDAEXPR in the buffer "*Normal Form*".<br>  This function goes to the beginning of the Agda comment in the<br>  current line, i.e., to the first occurrence of "--" in the<br>  current line, and the runs ‘C-c C-n AGDAEXPR RET’ there.<br>  This only works in agda2-mode. This is a quick hack!<br><br>If I go to the beginning of the line with the<br><br>  -- (find-agdanorm "aa +++ bb")<br><br>and I type `C-c C-n aa +++ bb RET' there - or if I execute the sexp -<br>Agda tells me that the _+++_ is not in scope, and the same happens<br>with this one here:<br><br>  -- (find-agdanorm "_+++_")<br><br>I get the same "Not in scope" if I use `C-c C-d _+++_' to get the type<br>of _+++_... but the last sexp,<br><br>  -- (find-agdanorm "cc")<br><br>works, and it shows that the normalized value of cc is this:<br><br>  "(AAA +_2 BBB)"<br><br>All the other sexps work as expected without errors.<br><br>Is that behavior documented? It seems that `C-c C-n' and `C-c C-d' are<br>ignoring some symbols that were brought into scope by this line,<br><br>  open          Add "2"<br><br>and for me this is unexpected & bad.<br><br>I am using Agda 2.6.1.3 - I don't have the current version here.<br>I've put more info, links, and a screenshot in this page:<br><br>  <a href="http://angg.twu.net/eev-agda.html">http://angg.twu.net/eev-agda.html</a><br><br>Thanks in advance!<br>  Eduardo Ochs<br>  <a href="http://angg.twu.net/#eev">http://angg.twu.net/#eev</a><br><div><br></div></div>