diff options
| author | Son Ho | 2023-07-19 19:03:17 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-19 19:03:17 +0200 |
| commit | 821b09b14794ebc2fe7b7047fc60fd56fb2cd107 (patch) | |
| tree | 832b5e29cfaf27e8986e7e4fafbac1f354adc83c /backends/lean/Base/Progress/Progress.lean | |
| parent | abee28555eb9f95b1c548cc17b9fe746bc982b56 (diff) | |
Fix a small issue with the persistent state of progress
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index 9c75ee3c..84053150 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -291,16 +291,15 @@ namespace Test set_option trace.Progress true - -- #eval do pspecClassAttr.getState - -- #eval showStoredPSpec - -- #eval showStoredPSpecClass + #eval showStoredPSpec + #eval showStoredPSpecClass -/- theorem Scalar.add_spec {ty} {x y : Scalar ty} + theorem Scalar.add_spec {ty} {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by progress - simp [*] -/ + simp [*] /- @[pspec] |