lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

doc: mention maxSteps setting in its error message

Open BoltonBailey opened this issue 1 year ago • 2 comments

This small PR changes the error message that triggers when simp reaches the maxSteps parameter to mention that this is a configurable setting and say what the name of the setting is.

BoltonBailey avatar Feb 09 '24 03:02 BoltonBailey

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-02-09 04:41:18)

leanprover-community-mathlib4-bot avatar Feb 09 '24 04:02 leanprover-community-mathlib4-bot

I don't think people will know what to do from this description alone

Kha avatar Feb 09 '24 09:02 Kha