MarkB generic Sections NuprlLIB Doc

Def rel_exp(T;R;n) == if n=0 x,y. x = y T else x,y. z:T. (x R z) & (z rel_exp(T;R;n-1) y) fi (recursive)

is mentioned

In prior sections: mb nat mb list 1


MarkB generic Sections NuprlLIB Doc