Commit 9b01e3d8 by Robbert Krebbers

### Fix some spacing.

parent 81022281
Pipeline #4240 passed with stage
in 5 minutes and 2 seconds
 ... ... @@ -37,10 +37,10 @@ Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) : (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y). Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed. Lemma decide_left`{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP. Proof. destruct (decide P) as [?|?]; [|contradiction]. f_equal. apply proof_irrel. Qed. Lemma decide_right`{Decision P} `{!ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP. Proof. destruct (decide P) as [?|?]; [contradiction|]. f_equal. apply proof_irrel. Qed. Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP. Proof. destruct (decide P); [|contradiction]. f_equal. apply proof_irrel. Qed. Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP. Proof. destruct (decide P); [contradiction|]. f_equal. apply proof_irrel. Qed. (** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the components is double negated, it will try to remove the double negation. *) ... ...
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