Skip to content
Snippets Groups Projects
Commit 822007c2 authored by David Swasey's avatar David Swasey
Browse files

Document why disjoint union doesn't work with .

parent f7094463
No related branches found
No related tags found
No related merge requests found
......@@ -2,7 +2,9 @@ From stdpp Require Export sets boolset.
From iris.algebra Require Export cmra sets.
Set Default Proof Using "Type".
(** Union CMRA for [boolset] (see [sets]). *)
(** Union CMRA for [boolset] (see [sets]). It doesn't seem possible,
without axioms, to show [##] decidable on [boolset], which is required
by the disjoint union CMRA's operation (see [set_disj_op]). *)
Section boolset.
Context `{EqDecision A}.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment