diff --git a/backends/lean/Base/Extensions.lean b/backends/lean/Base/Extensions.lean index 8093ff183..5f63c1b1c 100644 --- a/backends/lean/Base/Extensions.lean +++ b/backends/lean/Base/Extensions.lean @@ -31,7 +31,7 @@ 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, + addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insert k v) s) RBap.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) }