aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith
diff options
context:
space:
mode:
authorGravatar Ismail <ismail-s@users.noreply.github.com>2017-12-27 19:21:02 +0000
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-08 11:12:34 +0100
commit8957279df5d927334695aee64caf4f6af37f828d (patch)
treee3c10919265d3eb29de2627e310b4228853226ca /theories/Arith
parent7e319ad03aba413f3165b848eaf821b364f9291b (diff)
Document between and exists_between types.
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Between.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 9b4071085..ead08b3eb 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).