fix: header-data.bmp

leanprover · Sep 14, 2023 · f9b5a29 · f9b5a29
1 parent f730795
commit f9b5a29
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean
@@ -36,7 +36,7 @@ structure JsonModule where
   deriving FromJson, ToJson
 
 structure JsonHeaderIndex where
-  headers : List (String × String) := []
+  declarations : List (String × JsonDeclaration) := []
 
 structure JsonIndexedDeclarationInfo where
   kind : String
@@ -51,7 +51,7 @@ structure JsonIndex where
   instancesFor : HashMap String (RBTree String Ord.compare) := .empty
 
 instance : ToJson JsonHeaderIndex where
-  toJson idx := Json.mkObj <| idx.headers.map (fun (k, v) => (k, toJson v))
+  toJson idx := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v))
 
 instance : ToJson JsonIndex where
   toJson idx := Id.run do
@@ -70,7 +70,7 @@ instance : ToJson JsonIndex where
     return finalJson
 
 def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) : JsonHeaderIndex :=
-  let merge idx decl := { idx with headers := (decl.info.name, decl.header) :: idx.headers }
+  let merge idx decl := { idx with declarations := (decl.info.name, decl) :: idx.declarations }
   module.declarations.foldl merge index
 
 def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do