Eagerly add instances

Many definitions in game theory are hereditary. For instance, all options of a Numeric game are Numeric, all options of an Impartial game are Impartial, etc.

The definition addInstances provides a tactic which will eagerly apply all passed functions to all of the hypotheses, creating new ones in the process. The intended usage of this is to, for instance, apply Numeric.of_mem_moves to all hypotheses, and thus build all possible Numeric instances.

def addInstances (constants : Array Lean.Name) : Lean.Elab.Tactic.TacticM Unit

A tactic that eagerly adds instances by applying the functions in constants to every hypothesis.

Equations

• addInstances constants = Lean.Elab.Tactic.liftMetaTactic1 (instances✝ constants)