fix: re-support Prop valued instances

DocGen4/Process/DocInfo.lean

@@ -149,20 +149,22 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name,
     let info ← TheoremInfo.ofTheoremVal i
     if ← isProjFn i.name then
       return some <| theoremInfo { info with render := false }
+    else if ← isInstance i.name then
+      let info ← InstanceInfo.ofTheoremVal i
+      return some <| instanceInfo info
     else
       return some <| theoremInfo info
   | ConstantInfo.opaqueInfo i => return some <| opaqueInfo (← OpaqueInfo.ofOpaqueVal i)
   | ConstantInfo.defnInfo i =>
     if ← isProjFn i.name then
       let info ← DefinitionInfo.ofDefinitionVal i
       return some <| definitionInfo { info with render := false }
+    else if ← isInstance i.name then
+      let info ← InstanceInfo.ofDefinitionVal i
+      return some <| instanceInfo info
     else
-      if ← isInstance i.name then
-        let info ← InstanceInfo.ofDefinitionVal i
-        return some <| instanceInfo info
-      else
-        let info ← DefinitionInfo.ofDefinitionVal i
-        return some <| definitionInfo  info
+      let info ← DefinitionInfo.ofDefinitionVal i
+      return some <| definitionInfo  info
   | ConstantInfo.inductInfo i =>
     let env ← getEnv
     if isStructure env i.name then

DocGen4/Process/InstanceInfo.lean

@@ -40,23 +40,48 @@ def getInstPriority (name : Name) : MetaM (Option Nat) := do
   else
     return some priority
 
+private def InstanceInfo.ofDefinitionInfo (info : DefinitionInfo) (type : Expr) :
+    MetaM InstanceInfo  := do
+  let mut info := info
 
-def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
-  let mut info ← DefinitionInfo.ofDefinitionVal v
-
-  if let some priority ← getInstPriority v.name then
+  if let some priority ← getInstPriority info.name then
     info := { info with attrs := info.attrs.push s!"instance {priority}" }
 
-  let some className ← isClass? v.type | panic! s!"isClass? on {v.name} returned none"
-  if let some instAttr ← getDefaultInstance v.name className then
+  let some className ← isClass? type | panic! s!"isClass? on {info.name} returned none"
+  if let some instAttr ← getDefaultInstance info.name className then
     info := { info with attrs := info.attrs.push instAttr }
 
-  let typeNames ← getInstanceTypes v.type
+  let typeNames ← getInstanceTypes type
 
   return {
     toDefinitionInfo := info,
     className,
     typeNames,
   }
 
+def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
+  let info ← DefinitionInfo.ofDefinitionVal v
+  InstanceInfo.ofDefinitionInfo info v.type
+
+def InstanceInfo.ofTheoremVal (v : TheoremVal) : MetaM InstanceInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  /-
+  This is a bit of a shortcut but it avoids having to duplicate the instance infrastructure for
+  `Prop` and non-`Prop` valued instances for now. If we run into issues with this later on we
+  can still easily get the hack out as it is limited to this function.
+  -/
+  let info : DefinitionInfo := {
+    toInfo := info,
+    -- theorems can't be unsafe, only definitions
+    isUnsafe := false,
+    -- theorems can't have reducibility hints so just put default
+    hints := .regular 0,
+    -- theorems don't have equations of interest
+    equations := none,
+    -- theorems can't be noncomputable, only definitions
+    isNonComputable := false
+  }
+
+  InstanceInfo.ofDefinitionInfo info v.type
+
 end DocGen4.Process