Go backward to Typed Parameters Go up to Top Go forward to 2. Version

1. Version

Type-equivalence checker:

T': Type-structure -> Environment ->
    (Expressible-value + Errvalue)

(T'[[T]]e x)

• Determines whether x has type [[T]].
• If yes, result is inExpressible-value(x).
• If no, result is inErrvalue().

D[[proc I₁(I₂:T) = C]] = lambda e. lambda s.
    ((updateenv [[I₁]]
        inProc(lambda x. cases (T'[[T]]e x) of
            isExpressible-value(x) ->
                C[[C]](updateenv [[I]] x e)
            [] isErrvalue() -> signalerr end)
        e), (return s))