Commit 0d35f72e authored by Andrei Paskevich's avatar Andrei Paskevich

a couple of questions in ./TODO

parent 2502a2e7
......@@ -7,7 +7,14 @@ syntaxe
sémantique
----------
- 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.
- 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