Commit 2026-01-14 11:11 d4cb3b76

View on Github →

feat: rename HasCompl to Compl (#33545) This PR renames the HasCompl type class to Compl. This is consistent with all other notation classes, where the class name is the same as the operator name, but capitalized. (e.g. HAdd.hAdd, Max.max, Bot.bot). This also helps the automatic name translation in to_dual generate dual names (Compl is dual to HNot).

Estimated changes

modified theorem Pi.compl_apply
modified theorem Pi.compl_def
modified theorem Bool.compl_eq_bnot
modified theorem fst_compl
modified theorem snd_compl
modified theorem ULift.down_compl
modified theorem ULift.up_compl