diff options
Diffstat (limited to 'mathcomp/ssreflect/path.v')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index bccafa8..9327a2f 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -6,7 +6,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* The basic theory of paths over an eqType; this file is essentially a *) (* complement to seq.v. Paths are non-empty sequences that obey a progression *) (* relation. They are passed around in three parts: the head and tail of the *) -(* sequence, and a proof of (boolean) predicate asserting the progression. *) +(* sequence, and a proof of a (boolean) predicate asserting the progression. *) (* This "exploded" view is rarely embarrassing, as the first two parameters *) (* are usually inferred from the type of the third; on the contrary, it saves *) (* the hassle of constantly constructing and destructing a dependent record. *) @@ -16,7 +16,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* We allow duplicates; uniqueness, if desired (as is the case for several *) (* geometric constructions), must be asserted separately. We do provide *) (* shorthand, but only for cycles, because the equational properties of *) -(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat"). *) +(* "path" and "uniq" are unfortunately incompatible (esp. wrt "cat"). *) (* We define notations for the common cases of function paths, where the *) (* progress relation is actually a function. In detail: *) (* path e x p == x :: p is an e-path [:: x_0; x_1; ... ; x_n], i.e., we *) @@ -26,7 +26,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* the form [:: f x; f (f x); ...]. This is just a notation *) (* for path (frel f) x p. *) (* sorted e s == s is an e-sorted sequence: either s = [::], or s = x :: p *) -(* is an e-path (this is oten used with e = leq or ltn). *) +(* is an e-path (this is often used with e = leq or ltn). *) (* cycle e c == c is an e-cycle: either c = [::], or c = x :: p with *) (* x :: (rcons p x) an e-path. *) (* fcycle f c == c is an f-cycle, for a function f. *) @@ -47,9 +47,9 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* c (viewed as a cycle), or x if x \notin c. *) (* prev c x == the predecessor of the first occurrence of x in the *) (* sequence c (viewed as a cycle), or x if x \notin c. *) -(* arc c x y == the sub-arc of the sequece c (viewed as a cycle) starting *) +(* arc c x y == the sub-arc of the sequence c (viewed as a cycle) starting *) (* at the first occurrence of x in c, and ending just before *) -(* the next ocurrence of y (in cycle order); arc c x y *) +(* the next occurrence of y (in cycle order); arc c x y *) (* returns an unspecified sub-arc of c if x and y do not both *) (* occur in c. *) (* ucycle e c <-> ucycleb e c (ucycle e c is a Coercion target of type Prop) *) @@ -73,12 +73,12 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* of splitP will also simultaneously replace take (index x p) with p1 and *) (* drop (index x p).+1 p with p2. *) (* - splitPl applies when x \in x0 :: p; it replaces p with p1 ++ p2 and *) -(* simulaneously generates an equation x = last x0 p. *) +(* simultaneously generates an equation x = last x0 p. *) (* - splitPr applies when x \in p; it replaces p with (p1 ++ x :: p2), so x *) (* appears explicitly at the start of the right part. *) (* The parts p1 and p2 are computed using index/take/drop in all cases, but *) -(* only splitP attemps to subsitute the explicit values. The substitution of *) -(* p can be deferred using the dependent equation generation feature of *) +(* only splitP attempts to substitute the explicit values. The substitution *) +(* of p can be deferred using the dependent equation generation feature of *) (* ssreflect, e.g.: case/splitPr def_p: {1}p / x_in_p => [p1 p2] generates *) (* the equation p = p1 ++ p2 instead of performing the substitution outright. *) (* Similarly, eliminating the loop removal lemma shortenP simultaneously *) @@ -86,7 +86,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (* last x p'. *) (* Note that although all "path" functions actually operate on the *) (* underlying sequence, we provide a series of lemmas that define their *) -(* interaction with thepath and cycle predicates, e.g., the cat_path equation *) +(* interaction with the path and cycle predicates, e.g., the cat_path equation*) (* can be used to split the path predicate after splitting the underlying *) (* sequence. *) (******************************************************************************) |