feat: show documentation for Quot primitives

leanprover · Dec 18, 2024 · a2f46f4 · a2f46f4
1 parent 70fca3c
commit a2f46f4
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 8 deletions.
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
@@ -88,10 +88,6 @@ structure TheoremInfo extends Info
 Information about an `opaque` declaration.
 -/
 structure OpaqueInfo extends Info where
-  /--
-  The pretty printed value of the declaration.
-  -/
-  value : CodeWithInfos
   /--
   A value of partial is interpreted as this opaque being part of a partial def
   since the actual definition for a partial def is hidden behind an inaccessible value.

diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean
@@ -180,8 +180,8 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name,
   | ConstantInfo.ctorInfo i =>
     let info ← Info.ofConstantVal i.toConstantVal
     return some <| ctorInfo { info with render := false }
-  -- we ignore these for now
-  | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none
+  | ConstantInfo.quotInfo i => return some <| opaqueInfo (← OpaqueInfo.ofQuotVal i)
+  | ConstantInfo.recInfo _ => return none
 
 def getKindDescription : DocInfo → String
 | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"

diff --git a/DocGen4/Process/OpaqueInfo.lean b/DocGen4/Process/OpaqueInfo.lean
@@ -14,7 +14,6 @@ open Lean Meta
 
 def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
-  let value ← prettyPrintTerm v.value
   let env ← getEnv
   let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
   let definitionSafety :=
@@ -26,8 +25,14 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
       DefinitionSafety.safe
   return {
     toInfo := info,
-    value,
     definitionSafety
   }
 
+def OpaqueInfo.ofQuotVal (v : QuotVal) : MetaM OpaqueInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  return {
+    toInfo := info
+    definitionSafety := .safe
+  }
+
 end DocGen4.Process