Commit 2a39f248 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add example

parent 3d049510
......@@ -177,6 +177,22 @@ TODO: Algorithmic rules
TODO: test type system with $\lambda x:\pair{\Int}{\Int}\lor\pair{\Bool}{\Bool}. (\pi_1 x, \pi_2 x)$
TODO: Problem when typing the following:\\
x: Bool
let y = x in
let z = if y is True then (fun (z:True) -> true) else (fun (z:False) -> false)
in z x
The typing rules should return a list of pair (type, environments) in order to be
as precise as possible (= remember correlations). When typing a let, the candidates of $e_2$
should be computed under each possible environment of $e_1$ (in this way, we are sure that the
next operation will type (if possible)). Then, the candidate operator should return as soon
as it finds a required split, and it should be applied again and again until there
is no new split.
\subsection{Forward refinement rules}
\subsection{Backward refinement rules}
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