Skip to content
Snippets Groups Projects
Verified Commit 2f8891ae authored by Sankalp Gambhir's avatar Sankalp Gambhir
Browse files

Ex 5: Add missing rules (=, <=) in type system

parent b5d3fa3f
No related branches found
No related tags found
No related merge requests found
No preview for this file type
No preview for this file type
......@@ -32,7 +32,7 @@ around this system.
% integers
\AxiomC{\(n\) is an integer value}
\RightLabel{(int)}
\UnaryInfC{\(\Gamma \vdash \num(n) : \aint\)}
\UnaryInfC{\(\Gamma \vdash n : \aint\)}
\DisplayProof \\
% + -
\AxiomC{\(e_1 : \aint\)}
......@@ -65,6 +65,19 @@ around this system.
\RightLabel{(not)}
\UnaryInfC{\(\Gamma \vdash \neg e_1 : \abool\)}
\DisplayProof \\
% predicates
%% eq
\AxiomC{\(\Gamma \vdash e_1 : \tau\)}
\AxiomC{\(\Gamma \vdash e_2 : \tau\)}
\RightLabel{(eq)}
\BinaryInfC{\(\Gamma \vdash e_1 \lstinline|=| e_2 : \abool\)}
\DisplayProof \qquad
%% lte
\AxiomC{\(\Gamma \vdash e_1 : \aint\)}
\AxiomC{\(\Gamma \vdash e_2 : \aint\)}
\RightLabel{(lte)}
\BinaryInfC{\(\Gamma \vdash e_1 \lstinline|<=| e_2 : \abool\)}
\DisplayProof \\
% ite
\AxiomC{\(\Gamma \vdash e_1 : \abool\)}
\AxiomC{\(\Gamma \vdash e_2 : \tau\)}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment