diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-03-04 17:26:45 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2019-03-04 17:26:45 -0500 |
| commit | f9b2da9dd012e0ee0548aa82e8a132abc6429d7d (patch) | |
| tree | 7936f3736894a01af07bc7108082c30bc9700b5a /src/Util/Bool/Reflect.v | |
| parent | 9a6b540adee6440f36ce83c826ec291697f0dcf2 (diff) | |
Add some minor reflect things
Diffstat (limited to 'src/Util/Bool/Reflect.v')
| -rw-r--r-- | src/Util/Bool/Reflect.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Bool/Reflect.v b/src/Util/Bool/Reflect.v index d9e93fe93..8a5333f0a 100644 --- a/src/Util/Bool/Reflect.v +++ b/src/Util/Bool/Reflect.v @@ -69,6 +69,7 @@ Ltac beq_to_eq beq bl lb := Existing Class reflect. Definition decb (P : Prop) {b : bool} {H : reflect P b} := b. Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)). +Definition decb_rel {A B} (P : A -> B -> Prop) {b : A -> B -> bool} {H : reflect_rel P b} := b. Lemma decb_true_iff P {b} {H : reflect P b} : @decb P b H = true <-> P. Proof. symmetry; apply reflect_iff, H. Qed. |