Types somme IV
Typage des fonction définies par filtrage
Un cas
ë
(
x
1
:
t
1
),...,(
x
n
:
t
n
),
Env
û
|-
M
:
typ
1
ë
(
x
1
:
t
1
),...,(
x
n
:
t
n
),
Env
û
|-
exp
:
typ
2
Env
|-
function
M
->
exp
:
typ
1
®
typ
2
où les
x
i
sont les variables du motif
M
.
Plusieurs cas
Env
|- :
function
M
1
->
exp
1
:
typ
1
®
typ
2
...
Env
|- :
function
M
n
->
exp
n
:
typ
1
®
typ
2
Env
|-
function
|
M
1
->
exp
1
...
|
M
n
->
exp
n
:
typ
1
®
typ
2
