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

add type finiteness annotations for maps, sets, and bags

parent 801249ee
......@@ -7,6 +7,9 @@ theory Bag
type bag 'a
(** whatever ['a], the type [bag 'a] is always infinite *)
meta "infinite_type" type bag
(** the most basic operation is the number of occurrences *)
function nb_occ (x: 'a) (b: bag 'a): int
......@@ -7,6 +7,10 @@ theory Map
type map 'a 'b
(** if ['a] or ['b] are infinite types, then [map 'a 'b] is infinite *)
meta "material_type_arg" type map, 0
meta "material_type_arg" type map, 1
function get (map 'a 'b) 'a : 'b
function set (map 'a 'b) 'a 'b : map 'a 'b
......@@ -7,6 +7,9 @@ theory SetGen
type set 'a
(** if ['a] is an infinite type, then [set 'a] is infinite *)
meta "material_type_arg" type set, 0
(** membership *)
predicate mem 'a (set 'a)
Supports Markdown
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