NameDateSize

..25-Jul-20199

appFOLDLScript.smlH A D25-Jul-20195.4 KiB

basic_swapScript.smlH A D25-Jul-20194.4 KiB

binderLib.sigH A D25-Jul-20191.1 KiB

binderLib.smlH A D25-Jul-201920.3 KiB

generic_termsScript.smlH A D07-Jul-202052 KiB

HolmakefileH A D25-Jul-201926

mkterm.MLH A D07-Jul-202016.5 KiB

NEWLib.sigH A D25-Jul-2019116

NEWLib.smlH A D25-Jul-20191.5 KiB

nomdatatype.sigH A D25-Jul-20192 KiB

nomdatatype.smlH A D07-Jul-202011.5 KiB

nomsetScript.smlH A D08-Sep-202046.3 KiB

notes.txtH A D25-Jul-20194.1 KiB

precn.MLH A D07-Jul-20203.6 KiB

READMEH A D25-Jul-2019962

termScript.smlH A D22-Oct-202026.4 KiB

termSyntax.sigH A D25-Jul-2019555

termSyntax.smlH A D25-Jul-20191.7 KiB

README

1basic_swapScript.sml
2   Very basic theory of swaps over strings (the swapstr constant), and
3   permutations (which take a list of pairs of strings to swap).  Also
4   defines the NEW constant, which is used everywhere (including in
5   the dB and nc developments above).
6
7nomsetScript.sml
8   A more involved theory of permutations and their actions on
9   arbitrary types (the "nominal sets").  Includes the notion of
10   support.
11
12NEWLib.{sig,sml}
13   simple tactics to use with the NEW constant.
14
15binderLib.{sig,sml}
16   Tools for doing proofs with terms that include binders, including
17   function definition and facilities from NEWLib.
18
19pretermScript.sml termScript.sml
20   Using a quotient over raw syntax from pretermTheory, establishes a
21   type of lambda calculus terms, and defines substitution, the notion
22   of free variable and permutations over that type.  Proves some
23   simple lemmas about substitution.  For example,
24
25     lemma14a: |- [VAR x/x] t = t
26
27