From 9c324ade60adf9b37f4f7b49776bd2bb3a82d5e9 Mon Sep 17 00:00:00 2001
From: Parth Shastri <31370288+cppio@users.noreply.github.com>
Date: Thu, 19 Dec 2024 03:05:13 -0500
Subject: [PATCH] feat: show documentation for Quot primitives (#251)

---
 DocGen4/Process/Base.lean       | 4 ----
 DocGen4/Process/DocInfo.lean    | 4 ++--
 DocGen4/Process/OpaqueInfo.lean | 9 +++++++--
 3 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index 6395f2f6..0f595a6c 100644
--- 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
index 5ccf0e78..4f479698 100644
--- 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
index d85affa1..08641780 100644
--- 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