let sigma = unifylist((v1,Intero) :: (v2,Intero) :: (c1 @ c2)) in
match sigma with
|Fail -> (Forall([],Notype),[])
|Subst(s) -> (Forall([],Intero),s)
let f2 =newvar() in
let body = sem aa (bind(r,ii,(Forall([],f1),[]))) in
(match body with
| (Forall(_,t),c) -> let sigma = unifylist( (t,f2) :: c) in
(match sigma with
|Fail -> (Forall([],Notype),[])
|Subst(s) -> (Forall([],applysubst sigma (Mkarrow(f1,f2))),s)))
| Previous slide | Next slide | Back to first slide | View graphic version |