diff options
| author |  Ismail <ismail-s@users.noreply.github.com> | 2017-12-27 19:21:02 +0000 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-08 11:12:34 +0100 |
| commit | 8957279df5d927334695aee64caf4f6af37f828d (patch) | |
| tree | e3c10919265d3eb29de2627e310b4228853226ca /theories/Arith | |
| parent | 7e319ad03aba413f3165b848eaf821b364f9291b (diff) | |
Document between and exists_between types.
Diffstat (limited to 'theories/Arith')
| -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 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). |