TODO 438 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12

syntaxe
-------

  - le point (.) dans les noms qualifiés introduit un conflit dans la syntaxe 
    de forall/exists 	

		forall x : a. b
		forall x : a.b: c

    -> changement temporaire de syntaxe pour forall / exists : virgule
       plutôt que point
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
13 14 15 16 17 18 19


sémantique
----------
 
  - 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