#
d5cfabcb |
|
11-Dec-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Develop theory of finite sets, using developing transfer library Use our existing quotient library to create new type, but then transfer theorems using new technology. New entry-points in transferLib are mostly there to make debugging easier.
|
#
05695165 |
|
27-Nov-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Polish some fmspTheory results
|
#
a484d053 |
|
22-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More results about the finite-map/sptree connection I haven't forced it be a bijection (i.e, finite maps are allowed to be related to non-wellformed sptrees), in the hope that I will still to be able to figure out a good way of translating recursive definitions. Also put src/transfer into build sequence
|
#
abf57d25 |
|
19-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove flagged Unicode from previous commit
|
#
613c2bad |
|
19-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Start theories necessary to do "transfer" between fmaps and sptrees This being "transfer" in the style of the Isabelle package (Huffman and KunĨar).
|