Skip to content
Snippets Groups Projects
Commit 3e630f05 authored by Ralf Jung's avatar Ralf Jung
Browse files

dom: make D type agument name consistent

parent a389ce1b
No related branches found
No related tags found
1 merge request!376make dom domain type paremeter (D) implicit
Pipeline #65773 passed
...@@ -1304,10 +1304,10 @@ Global Instance: Params (@partial_alter) 4 := {}. ...@@ -1304,10 +1304,10 @@ Global Instance: Params (@partial_alter) 4 := {}.
Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert. Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [dom m] should yield the domain of [m]. That is a finite (** The function [dom m] should yield the domain of [m]. That is a finite
set of type [C] that contains the keys that are a member of [m]. set of type [D] that contains the keys that are a member of [m].
[C] is an output of the typeclass, i.e., there can be only one instance per map [D] is an output of the typeclass, i.e., there can be only one instance per map
type [M]. *) type [M]. *)
Class Dom (M C : Type) := dom: M C. Class Dom (M D : Type) := dom: M D.
Global Hint Mode Dom ! - : typeclass_instances. Global Hint Mode Dom ! - : typeclass_instances.
Global Instance: Params (@dom) 3 := {}. Global Instance: Params (@dom) 3 := {}.
Global Arguments dom : clear implicits. Global Arguments dom : clear implicits.
......
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