HOL

HOL copied to clipboard

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...

mn200

Implement Coq-style goal-matching tactic

4

An “ltac” is perhaps of the form ``` ([hyppat1, hyppat2, ...], goalpat, (fn ([matchvar1, matchvar2, ...], [hypth1, hypth2, ...], goalterm) => tactic)) ``` where the `hyppat` and `goalpat` are terms...

mn200

Use an efficient datastructure for substitution

2

Currently, functions like `match_term` return substitutions represented as a list of pairs. Why don't all these functions use maps instead of lists? ## Want to back this issue? **[Post a...

GallagherCommaJack

Binder-like syntax for {PROD,SUM}_IMAGE

1

`Π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...

mn200

Allow 'is alias of' entries in docfiles.

1

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...

mn200

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)**...

mn200

removing individual rewrites from a simpset

3

It would be nice to be able to remove things from simpsets (especially for interactive development, or when ensuring something does not get added in the first place is infeasible)....

xrchz

[Holyhammer] Easier interaction with Holyhammer in emacs/vim

3

Following Ramana's recent email to the users' list, I gave Holyhammer a try. Here're two features that, I think, would make interaction easier (in Vim or Emacs): 1) Shortcut to...

tanyongkiam

@konrad-slind has some technology for defining partial functions in an evaluation-friendly way. This issue is to ensure it eventually gets incorporated into the repository. ## Want to back this issue?...

xrchz

Finding out what a string might be printed/parsed as is useful for both terms and types. For terms, we have Parse.overload_info_for. For both there are various functions of the form...

xrchz