Def Lean.PrettyPrinter.Parenthesizer.Mathlib.CrossRef.getPiBaseTopic?

Modification history

2026-09-01 08:37
Mathlib/Tactic/CrossRefAttribute.lean
feat: implement pi-base cross-reference attribute (#41487) …
Added Lean.PrettyPrinter.Parenthesizer.Mathlib.CrossRef.getPiBaseTopic?View on Github →