diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 9209cecb268e77e2ab4e362fee28f01a91de98bf..07b0225e41a3f14033540171a89d74df8508c09f 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -142,8 +142,8 @@ Fixpoint map_seq `{Insert nat A M, Empty M} (start : nat) (xs : list A) : M := | x :: xs => <[start:=x]> (map_seq (S start) xs) end. -Instance finmap_lookup_total `{!Lookup K A (M A), !Inhabited A} : LookupTotal K A (M A) | 20 := - λ i m, default inhabitant (m !! i). +Instance finmap_lookup_total `{!Lookup K A (M A), !Inhabited A} : + LookupTotal K A (M A) | 20 := λ i m, default inhabitant (m !! i). Typeclasses Opaque finmap_lookup_total. (** * Theorems *)