test-claude.why 126 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9

theory Test

   use import int.Int

   goal Test1: 2+2 = 4

   goal Test2: forall x:int. x*x >= 0

MARCHE Claude's avatar
MARCHE Claude committed
10
   goal Test3: 1<>0 
MARCHE Claude's avatar
MARCHE Claude committed
11 12
end