From e6fe90b767c601df3933a39a01d8794543c13731 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Winterhalter?= Date: Fri, 29 May 2020 17:15:17 +0200 Subject: [PATCH] Remove more contractions --- chapters/coq-orders.tex | 2 +- chapters/coq-positions.tex | 2 +- chapters/elim-conclusion.tex | 2 +- chapters/elim-reflection-framework.tex | 2 +- chapters/elim-reflection-intro.tex | 2 +- chapters/flavours.tex | 2 +- chapters/translations.tex | 2 +- 7 files changed, 7 insertions(+), 7 deletions(-) diff --git a/chapters/coq-orders.tex b/chapters/coq-orders.tex index 565c320..7786ab2 100644 --- a/chapters/coq-orders.tex +++ b/chapters/coq-orders.tex @@ -122,7 +122,7 @@ \section{Constructive setting} end. \end{minted} It does not like the \mintinline{coq}{S n} bit in the recursive call. -I'm cheating a bit because it can still be defined by telling \Coq that +I am cheating a bit because it can still be defined by telling \Coq that \mintinline{coq}{S n} here is indeed a subterm of the matched term. \begin{minted}{coq} Fixpoint fib n := diff --git a/chapters/coq-positions.tex b/chapters/coq-positions.tex index 86151bd..67a1c49 100644 --- a/chapters/coq-positions.tex +++ b/chapters/coq-positions.tex @@ -375,7 +375,7 @@ \section{Ordering positions} the term, something which you cannot do indefinitely, you are bound to reach a leaf at some (finite) point. -If you think about it dually, I'm merely explaining that the structural order on +If you think about it dually, I am merely explaining that the structural order on terms is well-founded, so why bother? The interesting part is that the order on positions can be more flexible than the subterm relation in that it allows us to compare `going left' with diff --git a/chapters/elim-conclusion.tex b/chapters/elim-conclusion.tex index 0354438..61bd05d 100644 --- a/chapters/elim-conclusion.tex +++ b/chapters/elim-conclusion.tex @@ -6,7 +6,7 @@ \section{Limitations and Axioms} \label{sec:axioms} \marginnote[0.2cm]{ - I'd like to use a minimal representation of derivations that does not contain + I would like to use a minimal representation of derivations that does not contain everything that can be inferred automatically for one. } Currently, the representation of terms and derivations and the diff --git a/chapters/elim-reflection-framework.tex b/chapters/elim-reflection-framework.tex index efbd02e..d1212a2 100644 --- a/chapters/elim-reflection-framework.tex +++ b/chapters/elim-reflection-framework.tex @@ -785,7 +785,7 @@ \subsection{Typing of \acrshort{WTT}} % \end{mathpar} -You can notice that I'm cheating a little bit here. Indeed, I am already using +You can notice that I am cheating a little bit here. Indeed, I am already using heterogeneous equality (\(\cong\)) in the typing rules. If you would indulge me, you can imagine that the definition for heterogeneous equality is \emph{inlined} in the typing rules. That way it is a much more convenient read (and it is diff --git a/chapters/elim-reflection-intro.tex b/chapters/elim-reflection-intro.tex index 4f3cd21..a285ed2 100644 --- a/chapters/elim-reflection-intro.tex +++ b/chapters/elim-reflection-intro.tex @@ -21,7 +21,7 @@ \chapter{What I mean by elimination of reflection} This work gave rise to a publication~\sidecite[0.2cm]{winterhalter:hal-01849166} that focused on translating \acrshort{ETT} to \acrshort{ITT}. However, with Simon Boulier we worked on another version translating directly to -\acrshort{WTT} which I'm going to present here. +\acrshort{WTT} which I am going to present here. \section{Nature of the translation} diff --git a/chapters/flavours.tex b/chapters/flavours.tex index db7bfa9..7400e4e 100644 --- a/chapters/flavours.tex +++ b/chapters/flavours.tex @@ -396,7 +396,7 @@ \subsection{Inductive types} \emph{cumulative inductive types}~\sidecite{timany2018cumulative} (\acrshort{CIC}---and even \acrshort{CoC}---already has cumulativity). The idea is to extend the cumulativity relation beyond sorts to inductive types -as well. I'm going to use the same example than the paper introducing them: +as well. I am going to use the same example than the paper introducing them: a record~\sidenote{Exploiting the fact that (non-primitive) records are actually inductive types with one constructor in \Coq.} definition of categories: \[ diff --git a/chapters/translations.tex b/chapters/translations.tex index a85c961..238df9b 100644 --- a/chapters/translations.tex +++ b/chapters/translations.tex @@ -248,7 +248,7 @@ \section{Other translations} Sometimes, the empty context itself is not translated to the empty context as is the case in the forcing translation~\sidecite{jaber2016definitional} and such an encoding becomes impossible. -Even worse, in this document, in \arefpart{elim-reflection}, I'm going to +Even worse, in this document, in \arefpart{elim-reflection}, I am going to present a translation that is not even syntactic! Indeed, sometimes the translation can only be conducted at the derivation level: derivations in \cS are sent to derivations in \cT. It often reflects the fact that terms in \cS are