From d2b843289ab60a035d6493716b1c5dbe3d6de045 Mon Sep 17 00:00:00 2001 From: Marc-Antoine Ouimet Date: Sun, 29 May 2022 22:38:34 -0400 Subject: [PATCH] Add `{Plicity,Inductivity}.equal` --- src/core/inductivity.ml | 2 ++ src/core/inductivity.mli | 4 ++++ src/core/plicity.ml | 2 ++ src/core/plicity.mli | 4 ++++ 4 files changed, 12 insertions(+) diff --git a/src/core/inductivity.ml b/src/core/inductivity.ml index 243667652..2e827dabb 100644 --- a/src/core/inductivity.ml +++ b/src/core/inductivity.ml @@ -14,3 +14,5 @@ let max ind1 ind2 = let is_not_inductive = ( = ) not_inductive let is_inductive = ( = ) inductive + +let equal = ( = ) diff --git a/src/core/inductivity.mli b/src/core/inductivity.mli index 4a46b2991..ce8d6c5da 100644 --- a/src/core/inductivity.mli +++ b/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 diff --git a/src/core/plicity.ml b/src/core/plicity.ml index 772a5e962..6e169d83d 100644 --- a/src/core/plicity.ml +++ b/src/core/plicity.ml @@ -14,3 +14,5 @@ let max p1 p2 = let is_explicit = ( = ) explicit let is_implicit = ( = ) implicit + +let equal = ( = ) diff --git a/src/core/plicity.mli b/src/core/plicity.mli index 5eb9d9d07..596c5b463 100644 --- a/src/core/plicity.mli +++ b/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