diff --git a/src/js/controller/LogIndController.js b/src/js/controller/LogIndController.js index b77bdc1..f98c0d0 100644 --- a/src/js/controller/LogIndController.js +++ b/src/js/controller/LogIndController.js @@ -602,6 +602,21 @@ export class LogIndController extends ExerciseController { this.updateAlert('logind.error.caseNotRecognized', null, 'error') break } + if (term.includes('not basestep (not recognized)')) { + this.setErrorLocation(['formula-bottom', 'formula-top']) + this.updateAlert('logind.error.baseStepNotRecognized', null, 'error') + break + } + if (term.includes('not ihstep (not recognized)')) { + this.setErrorLocation(['formula-bottom', 'formula-top']) + this.updateAlert('logind.error.ihNotRecognized', null, 'error') + break + } + if (term.includes('not inductivestep (not recognized)')) { + this.setErrorLocation(['formula-bottom', 'formula-top']) + this.updateAlert('logind.error.inductiveStepNotRecognized', null, 'error') + break + } if (term.includes('not an instantiation')) { this.setErrorLocation(['formula-bottom', 'formula-top']) this.updateAlert('logind.error.notInstantiation', null, 'error') diff --git a/src/lang/en.json b/src/lang/en.json index c83f8c3..6070b6e 100644 --- a/src/lang/en.json +++ b/src/lang/en.json @@ -439,6 +439,7 @@ }, "completed": "The exercise is finished.", "error": { + "baseStepNotRecognized": "This is not a correct instantiation of a base case", "butBasestep": "This is not [[case]] but a base case for {{identifier}}", "butIhstep": "This is not [[case]] but an induction hypothesis for $${{identifier}}$$", "butInductivestep": "This is not [[case]] but an inductive case for $${{identifier}}$$", @@ -448,8 +449,10 @@ "differentMetaVarsWith": "Use the same metavariable in the first and second expression of the induction hypothesis, so $${{metaVar}}$$ in the second expression.", "doubleCase": "There is already a case $${{case}}$$, you need to prove exactly one case for each connective in the language.", "doubleIH": "You already formulated an induction hypothesis for $${{case}}$$.", + "ihNotRecognized": "This is not a correct induction hypothesis", "incorrect": "The proof contains an error.", "incorrectApplicationIh": "The application of the induction hypothesis is not correct.", + "inductiveStepNotRecognized": "This is not a correct instantiation of an inductive step", "invalidAtomsInInductiveCase": "Do not formulate inductive cases for compositions of atomic formulae, use the variables from the induction hypothesis.", "invalidBottomExpr": "The last expression of the subproof is not a correct instantiation of the right hand side of the theorem.", "invalidComposedBaseCase": "Only atomic cases belong to the base cases, composed formulae belong to the inductive cases.", diff --git a/src/lang/nl.json b/src/lang/nl.json index 8842f4a..e44cf32 100644 --- a/src/lang/nl.json +++ b/src/lang/nl.json @@ -439,6 +439,7 @@ }, "completed": "De uitwerking is compleet", "error": { + "baseStepNotRecognized": "Dit is geen correcte instantiatie van een basisstap", "butBasestep": "Dit is geen [[case]] maar een basis geval voor {{identifier}}", "butIhstep": "Dit is geen [[case]] maar een inductiehypothese voor $${{identifier}}$$", "butInductivestep": "Dit is geen [[case]] maar een inductief geval $${{identifier}}$$", @@ -448,8 +449,10 @@ "differentMetaVarsWith": "Gebruik dezelfde metavariabele in de eerste en tweede expressie van de inductiehypothese, dus een $${{metaVar}}$$ in de tweede expressie", "doubleCase": "Je hebt al een geval $${{case}}$$, voor elk connectief in de taal moet je precies 1 geval bewijzen.", "doubleIH": " je hebt al een inductiehypothese geformuleerd voor $${{case}}$$.", + "ihNotRecognized": "Dit is geen correcte inductiehypothese", "incorrect": "Er is een fout in het bewijs.", "incorrectApplicationIh": "De toepassing van de inductiehypothese is niet correct", + "inductiveStepNotRecognized": "Dit is geen correcte instantiatie van een inductiestap", "invalidAtomsInInductiveCase": "Formuleer de inductieve gevallen niet voor samenstellingen van atomaire formules, gebruik de variabelen uit de inductiehypothese", "invalidBottomExpr": "De laatste expressie van het deelbewijs is geen correcte instantie van de rechterkant van de stelling", "invalidComposedBaseCase": "Alleen atomaire gevallen horen tot de basisgevallen, samengestelde formules komen in de inductiestap aan bod",