test-pgm-jcf.mlx 529 Bytes
Newer Older
1 2 3

theory T
  type t = int
4 5 6 7 8 9 10
end

module M
  use import int.Int
  use import T
  function f (x: t) : t = x+1
  goal G: forall x: t. x=x
11

12 13 14
end

module N
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15
  use import int.Int
16 17
  use import M
  goal G1: f 41 = 42
18 19 20 21

  type tree 'a = Node 'a (forest 'a) | Leaf
  with forest 'a = Cons (tree 'a) (forest 'a) | Nil

Andrei Paskevich's avatar
Andrei Paskevich committed
22
  type ref 'b = {| ghost mutable contents : 'b |}
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23

Andrei Paskevich's avatar
Andrei Paskevich committed
24 25 26
  function id (tree 'c) : (tree 'c)

  let h (x : tree 'd) = ((id x) : tree 'd)
27 28 29 30 31 32 33
end

(*
Local Variables:
compile-command: "unset LANG; ../bin/why3ide test-pgm-jcf.mlx"
End:
*)