On the Definition of the Eta-long Normal Form in Type Systems of the Cube

07/03/2023
by   Gilles Dowek, et al.
0

The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not a sort then T < t is well-founded in the type systems of the cube. Thus every term admits a eta-long normal form.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset