diff options
| author | Son Ho | 2023-12-11 11:31:43 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-11 11:31:43 +0100 |
| commit | 10a77d17ea06b732106348588bedc6a89766d56f (patch) | |
| tree | 92a3cfabd788a2f74f71157e80b49f722d8d15f1 /backends/lean/Base/Progress/Progress.lean | |
| parent | 3c092169efcbc36a9b435c68c590b36f69204f94 (diff) | |
Reactivate the sanity checks for the progress tactic
Diffstat (limited to 'backends/lean/Base/Progress/Progress.lean')
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 93b7d7d5..a6a4e82a 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -245,7 +245,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL -- have the proper shape. let fExpr ← do let isGoal := true - withPSpec false isGoal goalTy fun desc => do + withPSpec isGoal goalTy fun desc => do let fExpr := desc.fArgsExpr trace[Progress] "Expression to match: {fExpr}" pure fExpr @@ -386,8 +386,6 @@ namespace Test progress keep _ as ⟨ z, h1 .. ⟩ simp [*, h1] - set_option trace.Progress false - example {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : |