-- This file:
--   http://angg.twu.net/AGDA/TestPublic.agda.html
--   http://angg.twu.net/AGDA/TestPublic.agda
--           (find-angg "AGDA/TestPublic.agda")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- Version: 20220201
-- Public domain.
--
-- See:      (find-angg "AGDA/find-agdatype.el")
--
-- (defun a () (interactive) (find-angg "AGDA/TestPublic.agda"))

module TestPublic 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

-- Local Variables:
-- coding:  utf-8-unix
-- End: