fix: work-around malformed all field in definitions

Export.lean

@@ -366,11 +366,13 @@ where
   theorems and definitions/opaques are still dumped in a singleton array for simplicity. -/
   dumpThmDefOpaque (base : ConstantInfo) : M Unit := do
     let mut all := #[]
-    for declarName in base.all do
-      let declar := (← read).env.find? declarName |>.get!
-      assert!((!declar.isUnsafe) || (← get).exportUnsafe)
-      all := all.push declar
-      modify fun st => { st with visitedConstants:= st.visitedConstants.insert declarName }
+    for declarName in (if base.all.contains base.name then base.all else base.name :: base.all) do
+      if declarName == base.name || !(← get).visitedConstants.contains declarName
+      then
+        let declar := (← read).env.find? declarName |>.get!
+        assert!((!declar.isUnsafe) || (← get).exportUnsafe)
+        all := all.push declar
+        modify fun st => { st with visitedConstants:= st.visitedConstants.insert declarName }
     for declar in all do
       dumpDeps declar.type
       dumpDeps (declar.value! (allowOpaque := true))

Main.lean

@@ -8,7 +8,7 @@ def exportMetadata : Json :=
   ]
   let exporterMeta := Json.mkObj [
     ("name", "lean4export"),
-    ("version", "3.0.0")
+    ("version", "3.1.0")
   ]
   let formatMeta := Json.mkObj [
     ("version", "3.0.0")

examples/Nat.add_succ.ndjson

@@ -1,4 +1,4 @@
-{"meta":{"exporter":{"name":"lean4export","version":"3.0.0"},"format":{"version":"3.0.0"},"lean":{"githash":"2fcce7258eeb6e324366bc25f9058293b04b7547","version":"4.27.0-rc1"}}}
+{"meta":{"exporter":{"name":"lean4export","version":"3.0.0"},"format":{"version":"3.0.0"},"lean":{"githash":"db93fe1608548721853390a10cd40580fe7d22ae","version":"4.27.0"}}}
 {"in":1,"str":{"pre":0,"str":"Nat"}}
 {"il":1,"succ":0}
 {"ie":0,"sort":1}