commit cc40084439f954f34ed4fdd29b51ed9ad1711be6
parent a2b462fc7fe46a71bae829d28eb1ed3b61c6a841
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Thu, 29 Jun 2017 20:26:10 +0200
Fixed LaTeX
Diffstat:
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/scribblings/tr.scrbl b/scribblings/tr.scrbl
@@ -985,7 +985,7 @@ therefore keep our overview succinct and gloss over most details.
vᵢ ∈ τᵢ ⇒ (v₁, …, vₙ) ∈ dom(f) ∧ f(v₁, …, vₙ) ∈ (τ'₁, …, τ'ₘ) \\
&@|quad|@where
(o₁, …, oₘ) ∈ (τ'₁, …, τ'ₘ) @textif oᵢ ∈ τ'ᵢ\\[1ex]
-
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
&@cat["fun"]{f} ∈ τ(∀ \textit{tvar} (τ₁, …, τₙ → τ'₁, …, τ'ₘ))\\
&@|quad|@where τ(∀ \textit{tvar₁} … \textit{tvarₖ} (τ₁, …, τₙ → τ'₁, …, τ'ₘ)) ∈ @u𝕋
&@|quad|@where υ⁺ = υ ∪ \{\textit{tvar₁} … \textit{tvarₖ}\}