www

commit 577d4a647601874de87ae53befb86f6a055d1162
parent cc40084439f954f34ed4fdd29b51ed9ad1711be6
Author: Georges Dupéron <georges.duperon@gmail.com>
Date:   Thu, 29 Jun 2017 20:26:50 +0200

Fixed LaTeX

Diffstat:
M
scribblings/tr.scrbl
 | 
6
+++---

1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/scribblings/tr.scrbl b/scribblings/tr.scrbl
@@ -987,9 +987,9 @@ therefore keep our overview succinct and gloss over most details.
    (o₁, …, oₘ) ∈ (τ'₁, …, τ'ₘ) @textif oᵢ ∈ τ'ᵢ\\[1ex]
    %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    &@cat["fun"]{f} ∈ τ(∀ \textit{tvar} (τ₁, …, τₙ → τ'₁, …, τ'ₘ))\\
-   &@|quad|@where τ(∀ \textit{tvar₁} … \textit{tvarₖ} (τ₁, …, τₙ → τ'₁, …, τ'ₘ)) ∈ @u𝕋
-   &@|quad|@where υ⁺ = υ ∪ \{\textit{tvar₁} … \textit{tvarₖ}\}
-   &@|quad|@textif τᵢ, τ'ⱼ ∈ 𝕋_{υ⁺} @;TODO: make @u𝕋 take an argument
+   &@|quad|@where τ(∀ \textit{tvar₁} … \textit{tvarₖ} (τ₁, …, τₙ → τ'₁, …, τ'ₘ)) ∈ @u𝕋 \\
+   &@|quad|@where υ⁺ = υ ∪ \{\textit{tvar₁} … \textit{tvarₖ}\} \\
+   &@|quad|@textif τᵢ, τ'ⱼ ∈ 𝕋_{υ⁺} \\ @;TODO: make @u𝕋 take an argument
    &@|quad|@textif
    ∀ \textit{instᵢ} ∈ @u𝕋, vⱼ ∈ σ(τⱼ)
    ⇒ (v₁, …, vₙ) ∈ dom(f) ∧ f(v₁, …, vₙ) ∈ (σ(τ'₁), …, σ(τ'ₘ)) \\