Add `lambdify` - also `oneline` + cheatsheet updates

HOL-Theorem-Prover / HOL

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.

https://hol-theorem-prover.org

Other

621 stars 140 forks source link

Add `lambdify` - also `oneline` + cheatsheet updates #1195

Closed hrutvik closed 7 months ago

hrutvik commented 7 months ago

Set up bossLib.lambdify, which should transform single-line definition theorems of the form |- ∀x y z. f x y z = ... to |- f = (\x y z. ...). This is a shorthand for DefnBase.LIST_HALF_MK_ABS, which is inspired by jrhUtils.HALF_MK_ABS.
lambdify is best used with one_line_ifyed definitions, so use bossLib.oneline as a shorthand for DefnBase.one_line_ify NONE.
Help docs + cheatsheet entries for both lambdify/oneline.
Also add eq_tac and ExclSF to the cheatsheet

mn200 commented 7 months ago

Can you at least mention, if not prefer, iff_tac as an alias for eq_tac please?

hrutvik commented 7 months ago

I hadn't even realised that alias existed 🤦 - added now!

mn200 commented 7 months ago

Fantastic; thanks!