#
6fe83575 |
|
12-Aug-2020 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
Add delete_delete thm to sptreeTheory
|
#
805c5015 |
|
26-May-2020 |
Andreas Lööw <AndreasLoow@users.noreply.github.com> |
Cleanup of append thms for SORTED
|
#
e2d0fafd |
|
14-Apr-2020 |
Heiko Becker <hbecker@mpi-sws.org> |
Remove redundant compute annotation
|
#
3c9809b4 |
|
07-Apr-2020 |
Heiko Becker <hbecker@mpi-sws.org> |
Move [compute] annotation for subspt to right place
|
#
2ff78aed |
|
14-Jan-2020 |
Thomas Sewell <sewell@chalmers.se> |
Replace unicode in previous
|
#
74da18e6 |
|
09-Jan-2020 |
Thomas Sewell <sewell@chalmers.se> |
Improve sptree toSortedAList Adding run-length-encoding to toSortedAList solves the problem with sparse trees, so toSortedAList is now respectably fast to EVAL in all cases. This version is slightly slower than the previous for packed trees, but it doesn't seem worth trying to fix that.
|
#
585f56f9 |
|
06-Jan-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Make num_map and num_set printing type abbreviations for sptrees
|
#
64a496f4 |
|
06-Jan-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Provide print-only syntax for ground sptree values E.g., > ``BN (LS v) (LS w)``; <<HOL message: inventing new type variable names: 'a>> val it = “⦕ 1 ↦ w; 2 ↦ v ⦖”: term There's a trace to turn it off. Considering enabling it as input syntax as well.
|
#
70c6fb7a |
|
16-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove older of Theorem syntaxes (the one with the quotes) It's confusing to allow two, and it seems pretty clear that the Proof-QED proof is nicer.
|
#
057a3046 |
|
15-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Deal with bad rebindings of theorems under src/ In bag, a name was reused for a different theorem so a name change was required. Elsewhere, the same theorem was stated and proved more than once so redundant stuff could be deleted.
|
#
5420e86d |
|
03-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Import a number of sptree theorems from CakeML Most about the subspt relation
|
#
e3821d79 |
|
31-Jan-2019 |
Thomas Sewell <sewell@chalmers.se> |
Remove copied unicode.
|
#
286add3e |
|
31-Jan-2019 |
Thomas Sewell <sewell@chalmers.se> |
Update for Theorem= syntax.
|
#
e6519a8f |
|
31-Jan-2019 |
Thomas Sewell <sewell@chalmers.se> |
Add toSortedAList to sptree. Adds an O(n) traversal of sptree's that extracts an association list sorted in index order. The absence of such a traversal was noted as a major drawback in the existing documentation. The algorithm is adapted from the one for Braun trees (sptree's are Braun trees with gaps/partiality added). It won't handle very sparse arrays well, that is, it's O(n) in the largest index, not the number of elements.
|
#
16920d84 |
|
24-Jan-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Start merging finite_map/dictionary theories into one directory Aim is to also include src/enumfset, possibly also the balanced_bst development from examples, and a CakeML theory (alist_tree). With all this stuff in the same place, we reduce branching under src/ and get better concurrency when building.
|