Add {Plicity,Inductivity}.equal

src/core/inductivity.ml

@@ -14,3 +14,5 @@ let max ind1 ind2 =
 let is_not_inductive = ( = ) not_inductive
 
 let is_inductive = ( = ) inductive
+
+let equal = ( = )

src/core/inductivity.mli

@@ -24,3 +24,7 @@ val is_not_inductive : t -> bool
 
 (** [is_inductive ind] is [true] if and only if [ind] is [Inductive]. *)
 val is_inductive : t -> bool
+
+(** [equal p1 p2] is [true] if and only if [p1] and [p2] are both [Explicit]
+    or [Implicit]. *)
+val equal : t -> t -> bool

src/core/plicity.ml

@@ -14,3 +14,5 @@ let max p1 p2 =
 let is_explicit = ( = ) explicit
 
 let is_implicit = ( = ) implicit
+
+let equal = ( = )

src/core/plicity.mli

@@ -30,3 +30,7 @@ val is_explicit : t -> bool
 
 (** [is_implicit p] is [true] if and only if [p] is [Implicit]. *)
 val is_implicit : t -> bool
+
+(** [equal p1 p2] is [true] if and only if [p1] and [p2] are both [Explicit]
+    or [Implicit]. *)
+val equal : t -> t -> bool