This branch is based on #544 branch for the equality checking.
The basic infrastructure for partial transformations is given:
Nucleus believes in transformations via the transformations module with add_rule (adds a transformation clause), act_judgement_abstraction (action of a transformation on a judgement abstraction) and act_boundary_abstraction (action of a transformation on a boundary abstraction)
the ML type system is extended with a new type transformation
The syntax is hard-coded as follows:
to specify a transformation: transformation | sym1 -> derivation1 | sym2 -> derivation2 | ... end
action of a transformation: map transf to jdg or map transf to bdry
an example (part of) FOL -> MLTT is given in the tests folder, see transformationFOLtoMLTT.m31.
Yet to discuss: syntax changes, error reporting, handling generated metavariables and scopes.
This branch is based on #544 branch for the equality checking.
The basic infrastructure for partial transformations is given:
Nucleus believes in transformations via the transformations module with
add_rule(adds a transformation clause),act_judgement_abstraction(action of a transformation on a judgement abstraction) andact_boundary_abstraction(action of a transformation on a boundary abstraction)the ML type system is extended with a new type
transformationThe syntax is hard-coded as follows:
transformation | sym1 -> derivation1 | sym2 -> derivation2 | ... endmap transf to jdgormap transf to bdryan example (part of) FOL -> MLTT is given in the tests folder, see
transformationFOLtoMLTT.m31.Yet to discuss: syntax changes, error reporting, handling generated metavariables and scopes.