Add `TCDiag` type class.

4c60de24 · Robbert Krebbers · 6c34b059 · 4c60de24
Commit 4c60de24 authored Feb 23, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

theories/base.v theories/base.v +5 -0

No files found.
--- a/theories/base.v
+++ b/theories/base.v
@@ -133,6 +133,11 @@ Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
 Existing Class TCEq.
 Existing Instance TCEq_refl.

+Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
+  | TCDiag_diag x : C x → TCDiag C x x.
+Existing Class TCDiag.
+Existing Instance TCDiag_diag.
+
 (** Throughout this development we use [stdpp_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope stdpp_scope with stdpp.