Commit 9b75ffdf authored by Robbert Krebbers's avatar Robbert Krebbers

Avoid overly long line.

parent b9d009d5
Pipeline #27359 passed with stage
in 13 minutes and 40 seconds
......@@ -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 *)
......
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