Skip to content

GitLab

why3
why3
Switch branch/tag
Find file Normal viewHistoryPermalink
test.why 71 Bytes
Newer Older
Jean-Christophe Filliâtre's avatar
mise en place de 'make test' qui teste src/test.why  
Jean-Christophe Filliâtre committed
1 2 3 

(* test file *)
Jean-Christophe Filliâtre's avatar
uses = declaration comme une autre ; retablissement du . dans la syntaxe de forall/exists  
Jean-Christophe Filliâtre committed
4 5 6 7 8 
theory A
  type t
end

theory B
Francois Bobot's avatar
ajout de théories dans test.why  
Francois Bobot committed
9 
  type t
Jean-Christophe Filliâtre's avatar
Theory : use  
Jean-Christophe Filliâtre committed
10 
  use A
Jean-Christophe Filliâtre's avatar
Typing utilise maintenant Theory  
Jean-Christophe Filliâtre committed
11 
end