Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
This adds a hook (which is normally set to do nothing) which is called whenever a preterm is elaborated. This is used in the VSCode editor mode so that it can record the locations of subterms together with typing information.
mn200
commented
1 week ago
This adds a hook (which is normally set to do nothing) which is called whenever a preterm is elaborated. This is used in the VSCode editor mode so that it can record the locations of subterms together with typing information.