Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Giuseppe Castagna
occurrence-typing
Commits
1c1bf33b
Commit
1c1bf33b
authored
Nov 24, 2020
by
Giuseppe Castagna
Browse files
rewording
parent
3c6c2c26
Changes
1
Hide whitespace changes
Inline
Side-by-side
new_system_beppe.tex
View file @
1c1bf33b
...
...
@@ -102,8 +102,11 @@ The idea is to translate terms above in to explicitly annotated
notrmal form and prove that a term above is well typed if and only if
its translation is well typed for a suitable annotation.
In particular the typing rule for cases will be obtained by combining
the union rule with the case rule and using two subsumption rules. Intuitively
In particular the typing rule for cases of CDuce will be obtained by combining
the union rule with the case rule and using two subsumption
rules. Intuitively we have that Cduce's
$
\tcase
{
x
\,
{
:
}{
=
}
\,
e
}
t
{
e
_
1
}{
e
_
2
}$
is
just syntactic sugar for
$
\letexp
x
{
e
}{
\tcase
{
x
}
t
{
e
_
1
}{
e
_
2
}}$
and
we have that:
\begin{mathpar}
\inferrule*
{
\inferrule*
{
...
...
@@ -120,8 +123,9 @@ the union rule with the case rule and using two subsumption rules. Intuitively
}
{
\Gamma\vdash
\letexp
x
{
e
}{
\tcase
{
x
}
t
{
e
_
1
}{
e
_
2
}
:t'
}}
\end{mathpar}
Note:
$
t
_
\circ
=(
t
\wedge
t
_
\circ
)
\vee
(
\neg
t
\wedge
t
_
\circ
$
)
[
Note:
$
t
_
\circ
=(
t
\wedge
t
_
\circ
)
\vee
(
\neg
t
\wedge
t
_
\circ
$
)
]
So we find exactly the typing rule for Cduce's typecase.
\subsubsection
{
Normal form terms with explicit annotations
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment