diff options
| author | Maxime Dénès | 2018-01-08 11:13:21 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-08 11:13:21 +0100 |
| commit | 60f1ca9942b7d5af667f4f438e254f00310fff89 (patch) | |
| tree | bd55c77042fcceb725be16cefebca2b0473882ca | |
| parent | 1c173af8d467d5a216f5e6616aac75529e2a46b7 (diff) | |
| parent | 8957279df5d927334695aee64caf4f6af37f828d (diff) | |
Merge PR #6510: Document between and exists_between types.
| -rw-r--r-- | theories/Arith/Between.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 9b40710858..ead08b3ebb 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -16,6 +16,8 @@ Implicit Types k l p q r : nat. Section Between. Variables P Q : nat -> Prop. + (** The [between] type expresses the concept + [forall i: nat, k <= i < l -> P i.]. *) Inductive between k : nat -> Prop := | bet_emp : between k k | bet_S : forall l, between k l -> P l -> between k (S l). @@ -47,6 +49,8 @@ Section Between. induction 1; auto with arith. Qed. + (** The [exists_between] type expresses the concept + [exists i: nat, k <= i < l /\ Q i]. *) Inductive exists_between k : nat -> Prop := | exists_S : forall l, exists_between k l -> exists_between k (S l) | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). |