diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Base.lean | 9 | ||||
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 9 |
2 files changed, 13 insertions, 5 deletions
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean index 785b9362..72438d40 100644 --- a/backends/lean/Base/Progress/Base.lean +++ b/backends/lean/Base/Progress/Base.lean @@ -153,6 +153,15 @@ structure PSpecClassAttr where ext : MapDeclarationExtension (NameMap Name) deriving Inhabited +-- TODO: the original function doesn't define correctly the `addImportedFn`. Do a PR? +def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) := + registerSimplePersistentEnvExtension { + name := name, + addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insert k v) s) RBMap.empty, + addEntryFn := fun s n => s.insert n.1 n.2 , + toArrayFn := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1) + } + /- The persistent map from function to pspec theorems. -/ initialize pspecAttr : PSpecAttr ← do let ext ← mkMapDeclarationExtension `pspecMap 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] |