r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: temporarily disable equation rendering

main
Henrik Böving 2023-11-18 23:06:55 +01:00
parent b85fd6cbeb
commit 8c9e5cf135
1 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
DocGen4/Process/DefinitionInfo.lean
View File

@ -36,8 +36,14 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
let info ← Info.ofConstantVal v.toConstantVal let info ← Info.ofConstantVal v.toConstantVal
let isUnsafe := v.safety == DefinitionSafety.unsafe let isUnsafe := v.safety == DefinitionSafety.unsafe
let isNonComputable := isNoncomputable (← getEnv) v.name let isNonComputable := isNoncomputable (← getEnv) v.name
try 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 match eqs? with
| some eqs => | some eqs =>
let equations ← eqs.mapM processEq let equations ← eqs.mapM processEq