Skip to content

Adding new constraint #414

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
BenEdV wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Adding new constraint #414

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c30b10b
Adding new constraint
BenEdV Sep 17, 2022
5717520
Add constraint for inductive step
BenEdV Sep 26, 2022
b9e819c
Merge branch 'main' into 412_new_constraint
BenEdV Sep 26, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 15 additions & 0 deletions src/js/controller/LogIndController.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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')
Expand Down
3 changes: 3 additions & 0 deletions src/lang/en.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}}$$",
Expand All @@ -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.",
Expand Down
3 changes: 3 additions & 0 deletions src/lang/nl.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}}$$",
Expand All @@ -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",
Expand Down