Michael Norrish
Michael Norrish
How do you learn what attributes are out there, and what they're for? ## --- Want to back this issue? **[Post a bounty on it!](https://www.bountysource.com/issues/36636819-document-theorem-attributes?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github)** We accept bounties via [Bountysource](https://www.bountysource.com/?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github).
In particular: - the `THEORY` data type should probably be in `Theory.sig` - there's no obvious reason why `DB` gets `print_theory` and `Hol_pp` doesn't. On the other hand, it's not...
If record has fields `foo` and `bar`, it's perfectly legitimate to write ``. The parser should warn you that you have missed out an initialisation for field `bar`. ## Want...
An interface to allow it easy to 1. add definitions by default to a custom compset 2. mark certain definitions as _not_ to be added 3. mark certain theorems as...
When parsing fails, it gives back useful numbers because the quotation filter puts line numbers into the quotation strings that are being parsed. Under Poly/ML, it might be possible to...
An “ltac” is perhaps of the form ``` ([hyppat1, hyppat2, ...], goalpat, (fn ([matchvar1, matchvar2, ...], [hypth1, hypth2, ...], goalterm) => tactic)) ``` where the `hyppat` and `goalpat` are terms...
`Πx ∈ s. x + 1` should parse to `PROD_IMAGE (λx. x + 1) s`. This is very similar to the transformation done in handling restricted quantifiers (which should also...
We have multiples across different structures (`bossLib` and `simpLib`) with the same name, and alternative spelling versions of others (_e.g._, `strip_tac` and `STRIP_TAC`). ## Want to back this issue? **[Post...
Something like ``` list = Nil | Cons (hd:'a) (tl:list) ``` (guessing at what the concrete syntax might be). ## Want to back this issue? **[Post a bounty on it!](https://www.bountysource.com/issues/28766782-allow-destructor-specifications-in-datatype?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github)**...