Re: pb with the Typol typechecker/Metal

[bertot@sophia.inria.fr (Yves Bertot)]

The Typol type-checker checks the correctness of your semantics
definition with respect to the abstract syntax of the language you
use.  If this abstract syntax is itself incoherent, then there is
no way the type-checker works properly.  I think this is your current
problem.  Please, look carefully at your "LG.metal" file and run the
"Check Metal" tool on it.  This may help you find your error yourself.
If this does not help, you may have to send the Metal source so that
we give you an opinion.

I hope this helps.

Yves Bertot.