Term.lazy_beta_conv, which is in turn called by Thm.Beta and Thm.Specialize.
Michael
On 12/4/18, 09:50, "Jeremy Dawson" <jeremy.daw...@anu.edu.au> wrote:
On 12/04/18 01:59, Mario Xerxes Castelán Castro wrote:
> for explicit lazy beta
> conversions (with an internal explicit substitution calculus)
I assume this refers to Clos, mk_clos etc in src/0/Term.sml
My questions is: is this actually used? I can't see where anything in
the source code creates a Clos where there isn't already one existing.
This would be odd, so I guess I've overlooked it somewhere - but where?
Jeremy
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
