equal
deleted
inserted
replaced
45 theory so that it is compatible with Higher-Order Logic, which the original formulation by |
45 theory so that it is compatible with Higher-Order Logic, which the original formulation by |
46 Pitts is not. We achieve this by not requiring that every construction has |
46 Pitts is not. We achieve this by not requiring that every construction has |
47 to have finite support. We present a formalisation that is based on a |
47 to have finite support. We present a formalisation that is based on a |
48 unified atom type and that represents permutations by bijective functions from |
48 unified atom type and that represents permutations by bijective functions from |
49 atoms to atoms. Interestingly, we allow swappings, which are permutations |
49 atoms to atoms. Interestingly, we allow swappings, which are permutations |
50 build from two atoms, to be ill-sorted. We also describe a formalisation of |
50 build from two atoms, to be ill-sorted. We also describe a reasoning infrastructure |
|
51 that automates properties about equivariance, and present a formalisation of |
51 two abstraction operators that bind sets of names. |
52 two abstraction operators that bind sets of names. |
52 \end{abstract} |
53 \end{abstract} |
53 |
54 |
54 % generated text of all theories |
55 % generated text of all theories |
55 \input{session} |
56 \input{session} |