def DocGen4.Process.OpaqueInfo.ofOpaqueVal (v : Lean.OpaqueVal) : Lean.MetaM OpaqueInfo

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.Process.OpaqueInfo.ofQuotVal (v : Lean.QuotVal) : Lean.MetaM OpaqueInfo

Equations

• DocGen4.Process.OpaqueInfo.ofQuotVal v = do let info ← DocGen4.Process.Info.ofConstantVal v.toConstantVal pure { toInfo := info, definitionSafety := Lean.DefinitionSafety.safe }