HOL

HOL copied to clipboard

Implement basic regex search functionality for DB.find

10

Hi, I've implemented some regex search support for DB.find based on issue #297 with a simple precedence parser. The grammar supports the previous two operators, in their same order of...

mrichards30

New example: Dijkstra's shortest path algorithm

8

myreen

The original implementation of toSortedAList was overcomplicated, using auxiliary run-length-encoding functions to carry across the idea of the algorithm from one that works on a dense structure. After a couple...

talsewell

Adds mrec and interp combinators to itreeTauTheory

3

This change introduces the `mrec` and `interp` combinators to `itreeTauTheory`. The mrec combinator is used extensively in the Pancake itree semantics.

xdrr

Rather than just output the term being examined, the monitoring function should be able to examine the term and return true/false to say whether or not computation should continue. If...

mn200

reorder and rename equantifiers by specifying pattern(s) underneath

1

If you don't want to rely on the order of the variables or their names, how do we pull the quantifier block into shape? The names in the pattern can...

mn200

As above

mn200

The quotation argument to this tactic specifies a pattern that will match one of the free `case` terms in the goal, and then do `Cases_on` that term. Avoids the need...

mn200