Q: Using TermInterface to set up Metatheory

Specific Domains Modelling & Simulations
, ,
1

While I have been using Symbolics and SymbolicUtils for some time now , I am a novice in the use of Metatheory.

My first attempt to set up Metatheory using TermInterface as described in the documentation is opened as an Issue in Metatheory:

I am having difficulty understanding the following code fragment in the documentation:

With

t = @theory a begin
  f(z(2), a) --> f(a)
end

in the code fragment

hcall = MyExpr(:h, [4], "hello")
ex = MyExpr(:f, [MyExpr(:z, [2]), hcall])
g = EGraph(ex; keepmeta = true)
  1. What is the symbolic expression :h in and the [4] correspond to in hcall = MyExpr(:h, [4], "hello")
  2. What does [2] correspond to in ex = MyExpr(:f, [MyExpr(:z, [2]), hcall])
  3. How do I convert this code fragment to my use case?

Any insight would be appreciated.