We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 1377325 commit b2cb9e5Copy full SHA for b2cb9e5
src/Lean/Meta/Tactic/Grind/AC/Action.lean
@@ -9,7 +9,7 @@ public import Lean.Meta.Tactic.Grind.Action
9
import Lean.Meta.Tactic.Grind.AC.Eq
10
namespace Lean.Meta.Grind.Action
11
12
-/-- Linear integer arithmetic action. -/
+/-- Associative-Commutative solver action. -/
13
public def ac : Action := fun goal kna kp => do
14
let (result, goal') ← GoalM.run goal AC.check
15
match result with
0 commit comments