Documentation

Lean.Meta.Tactic.Constructor

When the goal mvarId type is an inductive datatype, constructor calls apply with the first matching constructor.

Equations
    Instances For
      Equations
        Instances For