Hi Konrad,
Thank you very much! I’m learning finite_mapTheory now.
Regards,
Chun
> Il giorno 23 ott 2017, alle ore 20:42, Konrad Slind
> ha scritto:
>
> Hi Chun Tian,
>
> There are all kinds of issues with substitutions and applying them to
> term-like
> structures. I would probably sta
Hi Chun Tian,
There are all kinds of issues with substitutions and applying them to
term-like
structures. I would probably start by choosing finite maps
(finite_mapTheory) as
the representation for variable substitutions since they get rid of most if
not all
the issues with ordering of replaceme
Hi,
Suppose I have a list (or recursive structure defined by Datatype) in which
there’re some special elements marked as “variables”, e.g. ``var X``, ``var
Y``, … and I have a substitution function which correctly replaces a variable
into another closed term (i.e. term without variables), and
