Skip to content
Snippets Groups Projects

Improve comment of `TCEq`.

Merged Robbert Krebbers requested to merge robbert/tceq_comment into master
All threads resolved!
1 file
+ 6
4
Compare changes
  • Side-by-side
  • Inline
+ 6
4
@@ -195,10 +195,12 @@ Global Existing Instance TCElemOf_here.
@@ -195,10 +195,12 @@ Global Existing Instance TCElemOf_here.
Global Existing Instance TCElemOf_further.
Global Existing Instance TCElemOf_further.
Global Hint Mode TCElemOf ! ! ! : typeclass_instances.
Global Hint Mode TCElemOf ! ! ! : typeclass_instances.
(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
(** The intended use of [TCEq x y] is to use [x] as input and [y] as output, but
[TCEq] can also be used to unify evars. This is harmless: since the only
this is not enforced. We use output mode [-] (instead of [!]) for [x] to ensure
instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See
that type class search succeed on goals like [TCEq (if ? then e1 else e2) ?y],
https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)
see https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case.
 
Mode [-] is harmless, the only instance of [TCEq] is [TCEq_refl] below, so we
 
cannot create loops. *)
Inductive TCEq {A} (x : A) : A Prop := TCEq_refl : TCEq x x.
Inductive TCEq {A} (x : A) : A Prop := TCEq_refl : TCEq x x.
Existing Class TCEq.
Existing Class TCEq.
Global Existing Instance TCEq_refl.
Global Existing Instance TCEq_refl.
Loading