[Agda] Quirk: C-c C-n thinks that some symbols are not in scope

[Eduardo Ochs]

On Tue, 1 Feb 2022 at 17:01, Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi Eduardo,
>
> 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'.
>

 Hi Jesper!
Ooops and many many thanks!
I've added links to your explanation to the right places.
For the sake of completeness, here is a demo/test...

  module NameOfThisFile where

  open import Agda.Builtin.String
  open import Agda.Builtin.String.Properties

  infixl 4 _++_
  _++_ : String -> String -> String
  _++_ str1 str2 = primStringAppend str1 str2

  module Add (i : String) where
    infixl 4 _+_
    _+_ : String -> String -> String
    _+_ a b = "(" ++ a ++ " +_" ++ i ++ " " ++ b ++ ")"

  module Mul (i : String) where
    infixl 4 _*_
    _*_ : String -> String -> String
    _*_ a b = "(" ++ a ++ " *_" ++ i ++ " " ++ b ++ ")"

  module Add0 = Add "0"
  module Add1 = Add "1"
  open          Add "2" public
  open          Mul "3"           -- not "public"

  aa : String
  aa = "AAA"
  bb : String
  bb = "BBB"
  cc : String
  cc = aa + bb
  dd : String
  dd = aa * bb

  -- (find-agdanorm "aa ++ bb")
  -- (find-agdanorm "Add._+_   \"4\" aa bb")
  -- (find-agdanorm "Add0._+_        aa bb")
  -- (find-agdanorm "aa Add1.+          bb")
  -- (find-agdanorm "aa      +          bb")
  -- (find-agdanorm "_+_")
  -- (find-agdanorm "_*_")
  -- (find-agdanorm "cc")
  -- (find-agdanorm "dd")
  --
  -- Note that find-agdanorm considers that the _*_ is "Not in scope"...
  -- See: https://lists.chalmers.se/pipermail/agda/2022/012862.html
  --      https://lists.chalmers.se/pipermail/agda/2022/012863.html

Cheers =),
  Eduardo Ochs
  http://angg.twu.net/eev-agda.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220201/e7892a6b/attachment-0001.html>