Documentation

CustomPrelude.Linter.Semantic

Imports

Init
CustomPrelude.Linter.Semantic.BulletSubgoals
CustomPrelude.Linter.Semantic.ByExact
CustomPrelude.Linter.Semantic.ExistsIntro
CustomPrelude.Linter.Semantic.HypOrder
CustomPrelude.Linter.Semantic.RwaExactBare
CustomPrelude.Linter.Semantic.SelectorOneGoal
CustomPrelude.Linter.Semantic.SetNotLet
CustomPrelude.Linter.Semantic.UnfoldForeign
CustomPrelude.Linter.Semantic.UnusedHave

Imported by

Semantic linters #

The linter.fugue.* linters that read the InfoTree — goal states, name resolution, re-elaboration.