test-shape.why 256 Bytes
Newer Older
1 2 3

theory T

4 5 6 7 8
  use bool.Bool
  use int.Int
  use list.List
  use list.Length
  use list.Nth
9 10 11 12 13 14 15


  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

  goal g1: forall x:int. x >= 0 -> -x <= 0

end