Commit b916f997 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add idea

parent 1b2a70f6
......@@ -175,3 +175,8 @@ TODO: The $\evdash e t$ operator is used in the Case, OverApp and OverLet rules,
but what we would actually need is an operator that computes the other direction:
which environments can surely lead to $e$ having the type $t$?
(instead of: which environments are implied by $e$ having the type $t$)
TODO: Should we totally remove the Abs- rule and the type schemes from the paper
(and from the proof) and restricts the arrow type tests accordingly?
It would simplify a lot, it would match the implementation,
and we wouldn't have to bother with weird completeness results.
\ No newline at end of file
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