Documentation

Std.Lean.Parser

A simpArg is either a *, -lemma or a simp lemma specification (which includes the specifications for pre, post, reverse rewriting).

Instances For

    A simp args list is a list of simpArg. This is the main argument to simp.

    Instances For

      Extract the arguments from a simpArgs syntax as an array of syntaxes

      Instances For

        A dsimpArg is similar to simpArg, but it does not have the simpStar form because it does not make sense to use hypotheses in dsimp.

        Instances For

          A dsimp args list is a list of dsimpArg. This is the main argument to dsimp.

          Instances For

            Extract the arguments from a dsimpArgs syntax as an array of syntaxes

            Instances For