Commit 2025-01-13 11:11 7c7c15f0

View on Github →

feat: #count_heartbeats for all declarations (#20421) The "countHeartbeats" linter counts the heartbeats of every declaration. The effect of the linter is similar to #count_heartbeats in xxx, except that it applies to all declarations. Note that the linter only counts heartbeats in "top-level" declarations: it looks inside set_option ... in, but not, for instance, inside mutual blocks. There is a convenience notation #count_heartbeats that simply sets the linter option to true. Note. I also renamed count_heartbeats ... to #count_heartbeats .... Zulip

Estimated changes

added theorem XY'
added theorem XY
added theorem YX'
added theorem YX