On 11/04/18 18:45, michael.norr...@data61.csiro.au wrote:
> Could be done in principle, but I think the implementation (in particular, of 
> composition of substitutions) will likely be messy.

I see. I will attempt it sometime. For the moment it will go as an entry
in my personal to do list for HOL4.

> The paper behind the work introducing explicit substitutions is Barras, 
> TPHOLs 2000.

Thanks. I am reading this paper (I found the whole journal issue in
Library Genesis).

Do not eat animals; respect them as you respect people.

Attachment: signature.asc
Description: OpenPGP digital signature

Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
hol-info mailing list

Reply via email to