HOL
HOL copied to clipboard
HOL-Theorem-Prover
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.
The function `DB.find` function does a substring match. Why not extend to allow the string to be a regular expression. Along the way, we should allow an operator to allow...
Rather than just ``` ‘foo = bar’ by tac1 >> ‘_ = baz’ by tac2 >> ``` it should be possible to have stuff like ``` ‘foo = bar’ by...
Consider different behaviours of these three: ``` rw[Once FUNPOW] ([], ``p (FUNPOW f (SUC n) x) /\ q (FUNPOW g (SUC n) y)``); simp[Once FUNPOW] ([], ``p (FUNPOW f (SUC...
It's clearly useful to be able to see exactly what term is hiding underneath the `fld` of something like `r.fld`.
In particular, I think it should be possible to isolate sub-terms that include the excess type variables without just including the whole of the definition.
Similar to #488 but less extreme: Could we have a cache of theorems that have been proved before so that when this option is turned on any attempts to prove...
For `\HOLthm` and `\HOLtm`, it would be nice to “omit” certain sub-terms by specifying those terms in the optional arguments part of the command. Here “omit” means replace by “...”...
Support syntax for list comprehensions along the lines of ``` [ x + 1 | x α list -> β list`. This would then allow ``` [ x + y...
When parsing, the system doesn't do a paired β-reduction, and when printing, it doesn't recognise the term as an abstraction, and so fails to do any useful pattern-matching.
```` > Datatype`rcd = > val it = “∀x::r.fld. P x”: term ```` The printer should invert the parser here; without parentheses around the `r.fld`, the parser will fail to...
Metadata
Owner
Metadata
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.