test-jcf.why 416 Bytes
Newer Older
1 2


3

4
theory Records
5

6
  use import list.List
7
  use import bool.Bool
8
  use import int.Int
9

Andrei Paskevich's avatar
Andrei Paskevich committed
10 11 12
  namespace import R
    type t 'a 'b = {| a : 'a; b : list 'b; |}
  end
13

Andrei Paskevich's avatar
Andrei Paskevich committed
14
  goal g1 :
Andrei Paskevich's avatar
Andrei Paskevich committed
15 16
    let t = {| b = Cons True Nil; a = 1.0; |} in
    match {| t with a = 1 |} with
Andrei Paskevich's avatar
Andrei Paskevich committed
17 18 19
    | {| R.b = Cons x _ |} -> x = True
    | {| a = a |} -> a = 1
    end
20 21

end
22

Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
23 24
(*
Local Variables: 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25
compile-command: "make -C .. tests/test-jcf.gui"
Jean-Christophe Filliâtre's avatar
prelude  
Jean-Christophe Filliâtre committed
26 27
End: 
*)
28