Commit bf8cda8b authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify l/r-values.

parent 5fd6654b
......@@ -16,6 +16,7 @@ Instance listset_empty: Empty (listset A) := Listset [].
Instance listset_singleton: Singleton A (listset A) := λ x, Listset [x].
Instance listset_union: Union (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (l' ++ k').
Global Opaque listset_singleton listset_empty.
Global Instance: SimpleCollection A (listset A).
Proof.
......
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