diff options
Diffstat (limited to 'backends/lean/Base/Progress/Base.lean')
-rw-r--r-- | backends/lean/Base/Progress/Base.lean | 9 |
1 files changed, 9 insertions, 0 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 |