END restrict
restrict is the restriction operator on functions, allowing a function defined on a supertype to be applied to a subtype. Note that it is a conversion, so will be inserted automatically when needed.
restrict
[T:TYPE,
S:
TYPE
FROM
T,
R:TYPE]
:
THEORY
BEGIN
f:
VAR
[T-
>
R]
s:
VAR
S
restrict(f)(s):
R
=
f(s);
injective
restrict:
LEMMA
injective?(f)
IMPLIES
injective?(restrict(f))
%%(TCC)
restrict_of_inj_is_inj:
OBLIGATION
restrict
of
inj
is
inj:
JUDGEMENT
restrict((f:(injective?[T,
R])
))
HAS_TYPE
(injective?[S,
R])
END
restrict