# let multiset_abs,multiset_rep =
define_quotient_type "multiset" ("multiset_of_list","list_of_multiset")
`multisame:A list -> A list -> bool`;;
val multiset_abs : thm = |- multiset_of_list (list_of_multiset a) = a
val multiset_rep : thm =
|- (?x. r = multisame x) <=> list_of_multiset (multiset_of_list r) = r
For development of this example, see the documentation entries for
define_quotient_type "finiteset" ("finiteset_of_list","list_of_finiteset")
`\l1 l2. !a:A. MEM a l1 <=> MEM a l2`;;
val it : thm * thm =
(|- finiteset_of_list (list_of_finiteset a) = a,
|- (?x. r = (\l1 l2. !a. MEM a l1 <=> MEM a l2) x) <=>
list_of_finiteset (finiteset_of_list r) = r)