tests/test-shape.why

   1
   2 theory T
   3
   4   use bool.Bool
   5   use int.Int
   6   use list.List
   7   use list.Length
   8   use list.Nth
   9
  10
  11   goal G : forall l: list 'a. length l >= 3 -> exists i j:int, x:'a. i <> j /\ nth i l = Some x /\ nth j l = Some x
  12
  13   goal g1: forall x:int. x >= 0 -> -x <= 0
  14
  15 end