Commit 752d27aa authored by Robbert Krebbers's avatar Robbert Krebbers

Hints for reflexivity also on goals that are not identical.

parent 13680b70
......@@ -8,7 +8,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ={n}= x ⋅
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, format "x ≼{ n } y") : C_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (?x {_} ?x) => reflexivity.
Hint Extern 0 (?x {_} ?y) => reflexivity.
Record CMRAMixin A
`{Dist A, Equiv A, Unit A, Op A, Valid A, ValidN A, Minus A} := {
......
......@@ -5,7 +5,7 @@ Class Dist A := dist : nat → relation A.
Instance: Params (@dist) 3.
Notation "x ={ n }= y" := (dist n x y)
(at level 70, n at next level, format "x ={ n }= y").
Hint Extern 0 (?x ={_}= ?x) => reflexivity.
Hint Extern 0 (?x ={_}= ?y) => reflexivity.
Hint Extern 0 (_ ={_}= _) => symmetry; assumption.
Tactic Notation "cofe_subst" ident(x) :=
......
......@@ -16,7 +16,7 @@ Notation "(⋅)" := op (only parsing) : C_scope.
Definition included `{Equiv A, Op A} (x y : A) := z, y x z.
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
Hint Extern 0 (?x ?x) => reflexivity.
Hint Extern 0 (?x ?y) => reflexivity.
Instance: Params (@included) 3.
Class Minus (A : Type) := minus : A A A.
......
......@@ -209,9 +209,9 @@ Instance: Params (@equiv) 2.
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
Hint Extern 0 (_ _) => reflexivity.
Hint Extern 0 (?x ?y) => reflexivity.
Hint Extern 0 (_ _) => symmetry; assumption.
Hint Extern 0 (_ {_} _) => reflexivity.
Hint Extern 0 (?x {_} ?y) => reflexivity.
Hint Extern 0 (_ {_} _) => symmetry; assumption.
(** ** Operations on collections *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment