From 292b74b0a4f8db7efd3bbcb3e2dabe54a2c913a6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Dec 2025 15:32:30 +0100 Subject: [PATCH] chore: update `grind` docstring (#11654) This PR updates the `grind` docstring. It was still mentioning `cutsat` which has been renamed to `lia`. This issue was reported during ItaLean. --- src/Init/Grind/Tactics.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean index b41cedba7a..1f7db8f960 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -156,10 +156,10 @@ theorems and helps prevent an excessive number of instantiations. - `grind only [, ...]` is like `grind [, ...]` but does not use theorems tagged with `@[grind]`. - `grind (gen := )` sets the maximum generation. -### Linear integer arithmetic (`cutsat`) +### Linear integer arithmetic (`lia`) `grind` can solve goals that reduce to **linear integer arithmetic (LIA)** using an -integrated decision procedure called **`cutsat`**. It understands +integrated decision procedure called **`lia`**. It understands * equalities   `p = 0` * inequalities  `p ≤ 0` @@ -172,7 +172,7 @@ This *model-based* search is **complete for LIA**. #### Key options: -* `grind -cutsat` disable the solver (useful for debugging) +* `grind -lia` disable the solver (useful for debugging) * `grind +qlia` accept rational models (shrinks the search space but is incomplete for ℤ) #### Examples: @@ -297,7 +297,7 @@ syntax (name := grindTrace) /-- `cutsat` solves linear integer arithmetic goals. -It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `cutsat` solver. +It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver. Please use `grind` instead if you need additional capabilities. **Deprecated**: Use `lia` instead. @@ -307,7 +307,7 @@ syntax (name := cutsat) "cutsat" optConfig : tactic /-- `lia` solves linear integer arithmetic goals. -It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `cutsat` solver. +It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `lia` solver. Please use `grind` instead if you need additional capabilities. -/ syntax (name := lia) "lia" optConfig : tactic