Commit 994462dc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More curry.

parent 13ddd3df
Pipeline #66524 passed with stage
in 4 minutes and 25 seconds
...@@ -176,8 +176,7 @@ and [DK:=gset K]. *) ...@@ -176,8 +176,7 @@ and [DK:=gset K]. *)
Definition map_preimage `{FinMapToList K A MKA, Empty MADK, Definition map_preimage `{FinMapToList K A MKA, Empty MADK,
PartialAlter A DK MADK, Empty DK, Singleton K DK, Union DK} PartialAlter A DK MADK, Empty DK, Singleton K DK, Union DK}
(m : MKA) : MADK := (m : MKA) : MADK :=
map_fold map_fold (λ i, partial_alter (λ mX, Some $ {[ i ]} default mX)) m.
(λ i x, partial_alter (λ mX, Some ({[ i ]} default mX)) x) m.
Typeclasses Opaque map_preimage. Typeclasses Opaque map_preimage.
(** * Theorems *) (** * Theorems *)
......
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