Type class version of equality.

c8d58d4c · Robbert Krebbers · e37edc7e · c8d58d4c
Commit c8d58d4c authored Feb 02, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

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

No files found.
--- a/theories/base.v
+++ b/theories/base.v
@@ -99,6 +99,10 @@ Existing Class TCForall2.
 Existing Instance TCForall2_nil.
 Existing Instance TCForall2_cons.

+Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
+Existing Class TCEq.
+Existing Instance TCEq_refl.
+
 (** 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.