Here is the proposal to remove the ability to have unnamed axioms at least in the declarations, but possibly even in the *.kore files. Currently, this ability enables a class of bugs - someone may (from the K code) create an axiom that is unmatchable by the code (that matches only named axioms).
Here is the proposal to remove the ability to have unnamed axioms at least in the declarations, but possibly even in the *.kore files. Currently, this ability enables a class of bugs - someone may (from the K code) create an axiom that is unmatchable by the code (that matches only named axioms).