Documentation

Lean.Meta.Tactic.Simp.SimpAll

Instances For
    Instances For
      @[reducible, inline]
      Equations
        Instances For
          Equations
            Instances For
              def Lean.Meta.simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (stats : Simp.Stats := { }) :
              Equations
                Instances For