| #
8614552a |
|
05-Feb-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Functions for min and max added.
|
| #
9318dd65 |
|
12-Jan-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
A couple of bug fixes for these syntax manipulation functions:
* strip_mult was utterly wrong
* list_mk_{plus,mult} were building terms in the wrong order
|
| #
3c7de74f |
|
30-Jun-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Provide a function for returning the integer of a real number term,
as long as that term is actually an integer (i.e., of the form &n or
~&n for some natural number numeral n).
|
| #
1e80fb3f |
|
25-Jun-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Finished basic syntax support for the reals.
|
| #
2868da76 |
|
25-Jun-2003 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Slightly more than half an implementation of the obvious syntax functions
for the reals. Note that I have (arbitrarily) decided that 1 / 3 doesn't
qualify as a real "literal", though it has no better canonical form.
I may change my mind on this, or be open to persuasion.
Feel free to finish this off while I'm in bed :-)
|