Michael Norrish
Michael Norrish
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.
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...
This is due to the use of "magic" constants to stand for various components of the case expression before it is translated into its final form.