Commit 239363e8 authored by Andrei Paskevich's avatar Andrei Paskevich

new notes in TODO

parent c96639b6
......@@ -8,12 +8,15 @@ syntaxe
sémantique
----------
- should split_goal provide a "right-hand side only split"?
- produce reparsable tasks in Why3 format: how to preserve information about
the origins of symbols to be able to use drivers after reparsing?
- weak memoization in transformations has a disadvantage: if a task or a decl
is not changed by a transformation, it will stay in the hash table forever,
since the key is the value.
since the key is the value. Should we use generation numbers in arguments
and results of transformations?
- uses : pour l'instant, l'ordre des théories dans le fichier est important
i.e. les théories mentionnées par uses doivent être définies précédemment
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment