We register a simp attribute for the game_cmp tactic. This needs to be done in a separate file to where the tactic is defined.

def Parser.Attr.game_cmp : Lean.ParserDescr

Simp attribute for lemmas used in game_cmp.

Equations

• One or more equations did not get rendered due to their size.

def Parser.Attr.game_cmp_proc : Lean.ParserDescr

Simplification procedure

Equations

• One or more equations did not get rendered due to their size.