-
Notifications
You must be signed in to change notification settings - Fork 0
Home
Juneyoung Lee edited this page May 15, 2025
·
1 revision
Welcome to the hol-light-materials wiki!
More topics to add:
-
Examples to show how the type inference work
-
Introduction to important hol-light types: term, thm, conversions(term->thm), conversionals(conv->conv), tactic( goal -> goalstate), thm_tactic(thm->tactic), thm_tactical(thm_tactic->thm_tactic), and how to work with them together to achieve certain purpose, presumably examples will be helpful.
-
Where are all the tactics, rules and conversions that might be useful and how to navigate to find them. I think for this one, a rough summary list would be helpful.