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

-- (find-agdausermanualpage (+ 4 27) "3.2.11 Strings")
-- (find-agdausermanualtext (+ 4 27) "3.2.11 Strings")
-- (find-agdaprimfile "Agda/Builtin/Equality.agda")
-- (find-agdaprimfile "Agda/Builtin/Bool.agda")
-- (find-agdaprimfile "Agda/Builtin/Nat.agda")
-- (find-agdaprimfile "Agda/Builtin/Char.agda")
-- (find-agdaprimfile "Agda/Builtin/List.agda")
-- (find-agdaprimfile "Agda/Builtin/String.agda")
-- (find-agdaprimfile "Agda/Builtin/String/Properties.agda")
-- (find-es "agda" "precedence")

module TestStrings where

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

infixl 4 _++_
_++_ : String -> String -> String
_++_ a b = primStringAppend a b

infixl 4 _l4_
_l4_ : String -> String -> String
_l4_ a b = "(" ++ a ++ " l4 " ++ b ++ ")"

infixr 5 _r5_
_r5_ : String -> String -> String
_r5_ a b = "(" ++ a ++ " r5 " ++ b ++ ")"

foo : String
foo = "FOO"

-- (find-agdanorm "primStringAppend foo foo")
-- (find-agdanorm "foo ++ foo")
-- (find-agdanorm "foo l4 foo l4 foo")
-- (find-agdanorm "foo l4 foo r5 foo")
-- (find-agdanorm "foo r5 foo l4 foo")
-- (find-agdanorm "foo r5 foo r5 foo")

module M1 where
  m1a : String
  m1a = "AAA"
  foo2 : {!!}
  foo2 = {!!}

-- (find-agdanorm  "m1a")
-- (find-agdanormp "m1a")


{-
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
export LC_ALL=en_GB.UTF-8
agda -v 2 TestStrings.agda  | tee /tmp/o
# (find-es "agda" "loading-process")

-}




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