Maude-help mailing list

[Emmanuel Castro <emmanuel.castro AT laposte.net>]

Hello,

I would like to run the Church Rosser checker of CRCHC on a module
computed at meta level (something like :
sometransformation(upModule('SOME-MODULE))...)

The CRCHC command only takes the name of a module as argument, not a
metalevel expression.

Is there a not too complex way to run CRCHC as a 'reduce/rewrite'
expression? I checked the sources but it does not seem obvious?

Or else, is there a way to put a module computed at the meta-level
into the Full Maude model database.

At present, I can export the transformed module into a text file and
then load it, but it is not convenient.

Thank you for your answers

Emmanuel