Zulip Chat Archive
Stream: mathlib4
Topic: docgen equations for irreducible defs don't show content
Yakov Pechersky (Jul 08 2024 at 09:35):
Compare docs#fderiv and src#fderiv. The former says it's equal to an inaccessible "wrapped.1"
Last updated: May 02 2025 at 03:31 UTC