- Added a note about inversekeys in a role definition.
This commit is contained in:
parent
96e7a32bff
commit
8b30526a57
@ -1,5 +1,7 @@
|
|||||||
- Add '--untyped' check for typeflaw detection (instead of the fairly
|
- It is currently not well-defined to define inversekeys within a role:
|
||||||
vague '--match'.
|
this requires some work at instantiation, because instantiated term
|
||||||
|
couples should be added to the inverses list, and removed at
|
||||||
|
descruction.
|
||||||
- Warshall is taking a third of the time running.
|
- Warshall is taking a third of the time running.
|
||||||
- Make 'dirty' flag.
|
- Make 'dirty' flag.
|
||||||
- Make a push-graph structure, where old graphs are simply remembered?
|
- Make a push-graph structure, where old graphs are simply remembered?
|
||||||
@ -28,8 +30,7 @@
|
|||||||
int termSymbolEqual(Term t1, Term t2);
|
int termSymbolEqual(Term t1, Term t2);
|
||||||
Iteration through the termlist should be done by hand.
|
Iteration through the termlist should be done by hand.
|
||||||
- Maybe add warning for type of matching in the output, maybe stderr.
|
- Maybe add warning for type of matching in the output, maybe stderr.
|
||||||
|
Maybe all state-space bounding info should be displayed.
|
||||||
- SConstruct file should check whether ctags actually exists (avoiding
|
- SConstruct file should check whether ctags actually exists (avoiding
|
||||||
errors)
|
errors)
|
||||||
- Proof output should be XML, with an external converter to dot format.
|
- Proof output should be XML, with an external converter to dot format.
|
||||||
- Internal hash over input files (maybe after parsing?) and switch
|
|
||||||
structure. This would make a caching mechanism much easier.
|
|
||||||
|
Loading…
Reference in New Issue
Block a user