From 8c9e5cf1358b22f2236a8e48e80f6491221ebffd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 18 Nov 2023 23:06:55 +0100
Subject: [PATCH] fix: temporarily disable equation rendering

---
 DocGen4/Process/DefinitionInfo.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean
index c6255d5..14cfdac 100644
--- a/DocGen4/Process/DefinitionInfo.lean
+++ b/DocGen4/Process/DefinitionInfo.lean
@@ -36,8 +36,14 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
   let info ← Info.ofConstantVal v.toConstantVal
   let isUnsafe := v.safety == DefinitionSafety.unsafe
   let isNonComputable := isNoncomputable (← getEnv) v.name
+
   try
-    let eqs? ← getEqnsFor? v.name
+    -- Temporary workaround until
+    -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/maxRecDepth.20in.20getEqnsFor.3F/near/402917295
+    -- is adddressed
+    let eqs? : Option (Array Name) := none
+    -- let eqs? ←  getEqnsFor? v.name
+
     match eqs? with
     | some eqs =>
       let equations ← eqs.mapM processEq