Skip to content

Commit

Permalink
Fix typo fierst to first
Browse files Browse the repository at this point in the history
  • Loading branch information
mrs1669 committed Mar 19, 2024
1 parent 7da4934 commit 59b25c4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion docs/Generics/chapters/building-generic-signatures.tex
Original file line number Diff line number Diff line change
Expand Up @@ -628,7 +628,7 @@ \section{Requirement Validity}\label{generic signature validity}
\ldots\vdash \ConfReq{Self.Iterator}{IteratorProtocol}\tag{1}\\
(1)\vdash \texttt{Self.Iterator.Element}\tag{2}
\end{gather*}
Intuitively, anything we can say about the protocol \texttt{Self} type in this signature, is also true of an arbitrary type parameter \texttt{T.A.B} in some other generic signature $G$ where we can fierst derive the conformance requirement $\ConfReq{T.A.B}{Sequence}$. So a particular consequence of the above is that there ought to be a derivation of a valid type parameter \texttt{T.A.B.Iterator.Element} in $G$. We can show that this derivation always exists.
Intuitively, anything we can say about the protocol \texttt{Self} type in this signature, is also true of an arbitrary type parameter \texttt{T.A.B} in some other generic signature $G$ where we can first derive the conformance requirement $\ConfReq{T.A.B}{Sequence}$. So a particular consequence of the above is that there ought to be a derivation of a valid type parameter \texttt{T.A.B.Iterator.Element} in $G$. We can show that this derivation always exists.

We do this with a \IndexDefinition{formal substitution}\emph{formal substitution}. When writing down derivations, we've been doing formal substitution already. Each kind of derivation step is defined in the form of a ``schema,'' where it is understood the various meta-syntactic variables (\texttt{T} for type parameter, \texttt{P} for protocol, \texttt{A} for associated type, and so on) are replaced with concrete instances of those entities in some specific generic signature $G$. We can also imagine applying a formal substitution to an existing derivation, replacing some elements in a way that preserves the validity of the derivation.

Expand Down

0 comments on commit 59b25c4

Please sign in to comment.