A Type Checker for the exported files
We have written a type-checker (almost finished)
for the exported files to be sure that all the interesting information
was exported
The type-checker is used to check either theories or
single objects
Objects are not checked in the "static"
environment in which they were defined. An environment is dinamically
created during type-checking: when the t.c. finds a reference to
a not yet checked object, this one is recursively checked first.
Checks have been introduced to avoid (unsound)
cycles during the type-checking
PROBLEM: universe levels are inferred during type-checking
(as in Coq) ===> an object could be correct if checked alone, but not
with another one due to cycles in the universe constraints
(in Coq: two theory could be correct if required alone, but not if required
together. This is an example.)