break

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)
   }