Commit fcf2c1cc authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix unsound e7f8a2b6

parent bc135d79
...@@ -7,8 +7,7 @@ theory Map ...@@ -7,8 +7,7 @@ theory Map
type map 'a 'b type map 'a 'b
(** if ['a] or ['b] are infinite types, then [map 'a 'b] is infinite *) (** if ['b] is an infinite type, then [map 'a 'b] is infinite *)
meta "material_type_arg" type map, 0
meta "material_type_arg" type map, 1 meta "material_type_arg" type map, 1
function get (map 'a 'b) 'a : 'b function get (map 'a 'b) 'a : 'b
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment