Skip to content

fix: modify @[suggest_for] to work with the Prelude #20853

fix: modify @[suggest_for] to work with the Prelude

fix: modify @[suggest_for] to work with the Prelude #20853

check-lean-files

succeeded Dec 5, 2025 in 30s