equal
deleted
inserted
replaced
144 @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}. |
144 @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}. |
145 The problem with this definition is that we cannot follow the usual proofs |
145 The problem with this definition is that we cannot follow the usual proofs |
146 that are by induction on the type-part of the type-scheme (since it is under |
146 that are by induction on the type-part of the type-scheme (since it is under |
147 an existential quantifier and only an alpha-variant). The representation of |
147 an existential quantifier and only an alpha-variant). The representation of |
148 type-schemes using iterations of single binders |
148 type-schemes using iterations of single binders |
149 prevents us from directly ``unbinding'' the bound thye-variables and the type-part. |
149 prevents us from directly ``unbinding'' the bound type-variables and the type-part. |
150 The purpose of this paper is to introduce general binders, which |
150 The purpose of this paper is to introduce general binders, which |
151 allow us to represent type-schemes so that they can bind multiple variables at once |
151 allow us to represent type-schemes so that they can bind multiple variables at once |
152 and as a result solve this problem. |
152 and as a result solve this problem. |
153 The need of iterating single binders is also one reason |
153 The need of iterating single binders is also one reason |
154 why Nominal Isabelle and similar theorem provers that only provide |
154 why Nominal Isabelle and similar theorem provers that only provide |
2572 a corresponding reasoning infrastructure. However we have found out that |
2572 a corresponding reasoning infrastructure. However we have found out that |
2573 telescopes seem to not easily representable in our framework. The reason is that |
2573 telescopes seem to not easily representable in our framework. The reason is that |
2574 we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms. |
2574 we need to be able to lift our @{text bn}-function to alpha-equated lambda-terms. |
2575 This requires restrictions, which class with the `global' scope of binders in |
2575 This requires restrictions, which class with the `global' scope of binders in |
2576 telescopes. They can |
2576 telescopes. They can |
2577 be represented in the framework desribed in \cite{WeirichYorgeySheard11} using an extension of |
2577 be represented in the framework described in \cite{WeirichYorgeySheard11} using an extension of |
2578 the usual locally-nameless representation. |
2578 the usual locally-nameless representation. |
2579 |
2579 |
2580 \begin{figure}[p] |
2580 \begin{figure}[p] |
2581 \begin{boxedminipage}{\linewidth} |
2581 \begin{boxedminipage}{\linewidth} |
2582 \small |
2582 \small |