Skip to content

Commit

Permalink
Update src/Lean/Meta/Tactic/Grind/Arith/Offset.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Kim Morrison <scott.morrison@gmail.com>
  • Loading branch information
leodemoura and kim-em authored Jan 11, 2025
1 parent 1dc14c5 commit 5452eb5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Lean/Meta/Tactic/Grind/Arith/Offset.lean
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ where `k` is a numeral.
Each constraint is represented as an edge in a weighted graph.
The constraint `x ≤ y + k` is represented as a negative edge.
The shortest path between two nodes in the graph corresponds to an implied inequality.
nWhen adding a new edge, the state is considered unsatisfiable if the new edge creates a negative cycle.
When adding a new edge, the state is considered unsatisfiable if the new edge creates a negative cycle.
An incremental Floyd-Warshall algorithm is used to find the shortest paths between all nodes.
This module can also handle offset equalities of the form `x + k = y` by representing them with two edges:
```
Expand Down

0 comments on commit 5452eb5

Please sign in to comment.