[Merged by Bors] - refactor(Combinatorics/SimpleGraph): use edge and deleteEdges more#36804
[Merged by Bors] - refactor(Combinatorics/SimpleGraph): use edge and deleteEdges more#36804YaelDillies wants to merge 2 commits intoleanprover-community:masterfrom
edge and deleteEdges more#36804Conversation
PR summary 06a46dae32
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected | 588 | 589 | +1 (+0.17%) |
Import changes for all files
| Files | Import difference |
|---|---|
11 filesMathlib.Combinatorics.SimpleGraph.Connectivity.Connected Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Combinatorics.SimpleGraph.Metric |
1 |
Declarations diff
+ IsAcyclic.sup_edge_of_not_reachable
+ IsBridge.of_not_reachable
+ IsBridge.sup_edge_of_not_reachable
+ IsBridge.sup_edge_of_not_reachable_of_isBridge
+ deleteEdges_edge
+ deleteEdges_eq_bot
+ deleteEdges_le_iff
+ edgeSet_edge
+ edgeSet_edge_of_ne
+ edgeSet_edge_subset
+ edge_le
+ le_fromEdgeSet_iff
+ reachable_deleteEdges_iff_exists_walk
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
Alternatively, we should make them `abbrev`s.
YaelDillies
force-pushed
the
edge_delete_edges
branch
from
2579aa0 to
d212b37
Compare
github-actions
bot
removed
the
merge-conflict
b-mehta
left a comment
b-mehta
left a comment
There was a problem hiding this comment.
Clear win, nice.
Do you think we should make G \ fromEdgeSet s = G.deleteEdges s and fromEdgeSet {s(u, v)} = edge u v into simp lemmas to encourage this usage?
bors merge
#36804) Alternatively, we should make them `abbrev`s.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
edge and deleteEdges moreedge and deleteEdges more
I have thought about this, and I am not yet convinced enough to open a PR. A usability issue I have hit in similar cases is that this effectively forbids unfolding |
leanprover-community#36804) Alternatively, we should make them `abbrev`s.
leanprover-community#36804) Alternatively, we should make them `abbrev`s.
2 participants
Alternatively, we should make them
abbrevs.