Myott issueshttps://git.app.uib.no/Hakon.Gylterud/myott/-/issues2022-09-27T11:57:26+02:00https://git.app.uib.no/Hakon.Gylterud/myott/-/issues/14Variable lookup can fail for in Sequent.AST function constructTerm2022-09-27T11:57:26+02:00Håkon GylterudVariable lookup can fail for in Sequent.AST function constructTermIn some cases when an argument cannot be inferred, the `constructTerm` function has an in-exhaustive pattern.
We should investigate if there are cases which could be inferred better. If not then the user should be given indication of wh...In some cases when an argument cannot be inferred, the `constructTerm` function has an in-exhaustive pattern.
We should investigate if there are cases which could be inferred better. If not then the user should be given indication of which operations have insufficient arguments so that these can be specified. (What part of the code should have this responisibility?)https://git.app.uib.no/Hakon.Gylterud/myott/-/issues/11Prevent name collisions between judgements, operations and rules2021-08-03T13:28:37+02:00Håkon GylterudPrevent name collisions between judgements, operations and rulesCurrently there is no prevention against name collisions between judgments, operations and rules. The referees of each prevents internal collisions, but perhaps we should (because of calling conventions) prevent intercategorical collisions?Currently there is no prevention against name collisions between judgments, operations and rules. The referees of each prevents internal collisions, but perhaps we should (because of calling conventions) prevent intercategorical collisions?https://git.app.uib.no/Hakon.Gylterud/myott/-/issues/9Explicitly named arguments have unneeded parenthesis2021-08-03T11:22:49+02:00Håkon GylterudExplicitly named arguments have unneeded parenthesisCurrently the parser requires named arguments to have parenthesis, which is strictly not needed.
Example:
Hom { dom = (f x) , codom = y }
The parenthesis around `f x` are not needed, and we should instead parse it like this:
...Currently the parser requires named arguments to have parenthesis, which is strictly not needed.
Example:
Hom { dom = (f x) , codom = y }
The parenthesis around `f x` are not needed, and we should instead parse it like this:
Hom { dom = f x , codom = y }Elisabeth.BonnevierElisabeth.Bonnevierhttps://git.app.uib.no/Hakon.Gylterud/myott/-/issues/7Inference of propositional witnesses?2022-05-05T12:06:04+02:00Håkon GylterudInference of propositional witnesses?Propositions have unique witnesses in any context. Could we allow these to be unmentioned, and infer them when applying judgements and operations?
Note that this inference goes the opposite way of the dependency based inference, so
the ...Propositions have unique witnesses in any context. Could we allow these to be unmentioned, and infer them when applying judgements and operations?
Note that this inference goes the opposite way of the dependency based inference, so
the interplay between these two might be complicated.https://git.app.uib.no/Hakon.Gylterud/myott/-/issues/2Add haddock documentation2021-02-16T23:25:20+01:00Håkon GylterudAdd haddock documentationThe code needs to be much better documented. A good start would be to use Haddock to document the functions
and data structures.The code needs to be much better documented. A good start would be to use Haddock to document the functions
and data structures.https://git.app.uib.no/Hakon.Gylterud/myott/-/issues/1Lint all files2020-11-11T23:04:54+01:00Håkon GylterudLint all filesAt the moment only some files are linted by lint.sh.
But we should fix the suggestions given by hlint for other files as well.At the moment only some files are linted by lint.sh.
But we should fix the suggestions given by hlint for other files as well.