#
cad894cc |
|
20-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix lambda/typing example given 'perm_type' changes.
|
#
bc294d17 |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extract a usable half-way point from nominal_datatype branch. This replaces the is_perm predicate with a type embodying that predicate. It doesn't include the subsequent work on allowing multiple 'atom' types.
|
#
15f66f6f |
|
06-Jun-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get lambda/typing directory to build again. Had to deal with termScript stealing the \rightarrow syntax (I made that theft local to termScript); and with tight equality.
|
#
c0464c4e |
|
25-Jun-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Minor tidy-ups to sttScript; no long need to Unicode trace, for example.
|
#
0656585b |
|
02-Mar-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Tidy up typing proofs (more Unicode!), and fix a proof broken by LIST_EQ_SIMP.
|
#
39640ac1 |
|
01-Apr-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Hrumph. Even though the parser knows nothing of "B", CHOOSE_THEN or some other deep dark internal is still deciding to prime B when it appears in an assumed theorem like "?B. ..." This breaks the hastype_lam_inv proof. I fix it for the moment to use entirely different names, but am going to look into the other behaviour too. Compare: STRIP_TAC ([], ``(?B. P B) ==> P A``) and STRIP_TAC ([], ``!B. P B ==> P A``) The first primes B, the second doesn't. (In a standard hol install, replace B with C and you should see something similar because of C's presence as a constant in combinTheory.)
|
#
c25eeb9c |
|
31-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Explicitly hide the "B" combinator that I just introduced in chap2Theory so that I can continue to use it as a free variable name in my simple typing theory. (That's the problem with those dang combinators.)
|
#
2b2a6705 |
|
27-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fiddle and prettify basic presentation of beta-reduction. Using syntactic patterns, I can now have ``compat_closure beta M N`` (the "compatible closure of the beta-relation) appear as ``M -b-> N``. Also use syntactic patterns to get rid of constants reduction and conversion. Finally, provide Unicode versions of the various arrow symbols so that with the Unicode flag on, the above will come out as M -β-> N Even in just ASCII, I think the theorems look a deal prettier.
|
#
31704bbd |
|
23-Dec-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Modify release notes to reflect improvement in lexing, and make use of new facilities in simple type theory example.
|
#
176a481a |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes for these examples, and an updated MANIFEST/README in other-models. The other-models directory had become particularly stale. I obviously need to check that it works more often. (Main problem: change to behaviour of Q.INST.)
|
#
d35e23a5 |
|
06-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Continue to make the typing sub-directory of the lambda-calculus example as Unicodified as possible, as a general test-case of what the technology allows. (Now I can have Unicode universals as binders in Hol_reln calls, and Unicode strings as bound variables.)
|
#
3c56e7d4 |
|
26-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Unicode prettification.
|
#
effc431b |
|
01-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change export_rewrites back to its old API (without requiring an extra string). When exported, the resulting simpset fragment always picked up the name of the theory to be the base of its name, so there didn't seem much point in giving users a false impression of naming power.
|
#
78640b51 |
|
17-Sep-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make the typing relation look even prettier by using Unicode characters corresponding to LaTeX's \vdash and \lhd in the concrete syntax. (The ASCII version is still around and can be used for input too.)
|
#
ee7d0a45 |
|
09-Sep-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make this theory even more Unicodified.
|
#
1f53b889 |
|
30-Aug-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Refactor simple type theory development by moving theory of contexts as association lists on strings to a separate theory.
|
#
51fac28d |
|
27-Aug-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make a new directory containing some work on simple typing for the lambda calculus.
|