diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
| commit | 0ae5f6871b29d20f48b5df6dab663b5a44162d01 (patch) | |
| tree | 33b11090af2555a91a593f9b919edf83c71557cd /src/Experiments | |
| parent | a0bdb14300aa57eed684992a23a57fd319ef97c0 (diff) | |
remove trailing whitespace from src/
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 9a6873bba..33fdb5a17 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -46,7 +46,7 @@ Lemma Let_In_Proper_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB : Proper (RA ==> RB) (fun x => Let_In x f). Proof. intuition. Qed. -Ltac fold_identity_lambdas := +Ltac fold_identity_lambdas := repeat match goal with | [ H: appcontext [fun x => ?f x] |- _ ] => change (fun x => f x) with f in * | |- appcontext [fun x => ?f x] => change (fun x => f x) with f in * @@ -285,7 +285,7 @@ Proof. intros. pose proof (eqb_eq_dec' eqb eqb_iff a b). destruct (eqb a b); eauto. -Qed. +Qed. Lemma eqb_compare_encodings {T} {B} {encoding:canonical encoding of T as B} (T_eqb:T->T->bool) (T_eqb_iff : forall a b:T, (T_eqb a b = true) <-> a = b) @@ -308,7 +308,7 @@ Proof. pose proof encoding_valid. congruence. Qed. Lemma compare_without_decoding {T B} (encoding_T_B:canonical encoding of T as B) (T_eqb:T->T->bool) (T_eqb_iff:forall a b, T_eqb a b = true <-> a = b) (B_eqb:B->B->bool) (B_eqb_iff:forall a b, B_eqb a b = true <-> a = b) - (P_:B) (Q:T) : + (P_:B) (Q:T) : option_rect (fun _ : option T => bool) (fun P : T => T_eqb P Q) false |