Commit 819cb296 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Remove a footnote in algorithm that is not really needed.

parent 146d51c7
......@@ -9,12 +9,17 @@ types for the same well-typed expression and $(ii)$~how to compute the
auxiliary deduction system for paths.
$(i)$. Multiple types have two distinct origins each requiring a distinct
technical solution. The first origin is the presence of structural
rules\footnote{\label{fo:rules}In logic, logical rules refer to a
technical solution. The first origin is the presence of
%structural
rules
\iffalse
\footnote{\label{fo:rules}In logic, logical rules refer to a
particular connective (here, a type constructor, that is, either
$\to$, or $\times$, or $b$), while identity rules (e.g., axioms and
cuts) and structural rules (e.g., weakening and contraction) do
not.} such as \Rule{Subs} and \Rule{Inter}. We handle this presence
not.}
\fi
such as \Rule{Subs} and \Rule{Inter}. We handle this presence
in the classic way: we define an algorithmic system that tracks the
miminum type of an expression; this system is obtained from the
original system by removing the two structural rules and by
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment