Documentation

CustomPrelude.Linter.Syntax.RenameI

linter.fugue.renameI #

rename_i and expose_names reach for a hypothesis by its position in the context — the one thing every edit above them changes, silently. Name it where it is bound (rintro/obtain pattern, case/with alternative), or with next x y => …, or do not name it at all.

Syntax quotations are exempt — split … using and injections with build rename_i into themselves so no proof has to write it.