diff options
| author | Cyril Cohen | 2019-03-20 09:57:38 +0100 |
|---|---|---|
| committer | GitHub | 2019-03-20 09:57:38 +0100 |
| commit | 8b66255d1206368fec3b652aa2e3806d01193668 (patch) | |
| tree | 6ee67b70d944ae08c19a8326a88c9edca51bd4b2 /mathcomp | |
| parent | 4c8455594c5adff08761037a5919c058d0d502ba (diff) | |
| parent | d1d511b6b65109ed561ab158d0b231f399d4c01c (diff) | |
Merge pull request #300 from erikmd/doc-detail
[doc] Mention that "connect" computes the reflexive transitive closure
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/fingraph.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 5358dc7..1a0f25f 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -14,7 +14,7 @@ Require Import ssrbool ssrfun eqtype ssrnat seq path fintype. (* dfs g n v x == the list of points traversed by a depth-first search of *) (* the g, at depth n, starting from x, and avoiding v. *) (* dfs_path g v x y <-> there is a path from x to y in g \ v. *) -(* connect e == the transitive closure of e (computed by dfs). *) +(* connect e == the reflexive transitive closure of e (computed by dfs). *) (* connect_sym e <-> connect e is symmetric, hence an equivalence relation. *) (* root e x == a representative of connect e x, which is the component *) (* of x in the transitive closure of e. *) |