bench/check-ce/model_projection2.mlw

   1 module Type_Map
   2    type poly_map 'a 'b
   3    meta "encoding:ignore_polymorphism_ts" type poly_map
   4 end
   5
   6 module N
   7 use Type_Map
   8 type t
   9 type c
  10 type u = poly_map t c
  11
  12 function get (a : u) (i : t) : c
  13
  14 function to_array u : t -> c
  15 meta "model_projection" function to_array
  16 axiom to_array_get : forall x:u, i:t. to_array x i = get x i
  17
  18 function set (a : u) (i : t) (v : c) : u
  19
  20 end
  21
  22 module G
  23 use int.Int
  24 clone export N with type t = int, type c = int
  25 let g2 (x: u) : unit =
  26   assert {get x 13 < 41}
  27 end