Documentation

Batteries.Tactic.Alias

The alias command #

The alias command is used to create synonyms. The plain command can create a synonym of any declaration. There is also a version to create synonyms for the forward and reverse implications of an iff theorem.

An alias can be in one of three forms

Instances For

    The docstring for an alias.

    Equations
    Instances For

      Get the alias information for a name

      Equations
      Instances For

        Set the alias info for a new declaration

        Equations
        Instances For

          Updates the deprecated declaration to point to target if no target is provided.

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

            The command alias name := target creates a synonym of target with the given name.

            The command alias ⟨fwd, rev⟩ := target creates synonyms for the forward and reverse directions of an iff theorem. Use _ if only one direction is required.

            These commands accept all modifiers and attributes that def and theorem do.

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

              Given a possibly forall-quantified iff expression prf, produce a value for one of the implication directions (determined by mp).

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

                The command alias name := target creates a synonym of target with the given name.

                The command alias ⟨fwd, rev⟩ := target creates synonyms for the forward and reverse directions of an iff theorem. Use _ if only one direction is required.

                These commands accept all modifiers and attributes that def and theorem do.

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