Documentation

Aesop.RuleTac.Forward.Basic

Prefix of the regular hyps added by forward.

Equations
Instances For

    Prefix of the implDetail hyps added by forward.

    Equations
    Instances For

      Name of the implDetail hyp corresponding to the forward hyp with name fwdHypName and depth depth.

      Equations
      Instances For

        Parse a name generated by forwardImplDetailHypName, obtaining the fwdHypName and depth.

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

          Check whether the given name was generated by forwardImplDetailHypName. We assume that nobody else adds hyps with the forwardImplHypDetailPrefix prefix.

          Equations
          Instances For
            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                Instances For
                  • Types of the hypotheses that have already been added by forward reasoning.

                  • Depths of the hypotheses that have already been added by forward reasoning.

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

                        Mark hypotheses that, according to their name, are forward implementation detail hypotheses, as implementation details. This is a hack that works around the fact that certain tactics (particularly anything based on the revert-intro pattern) can turn implementation detail hyps into regular hyps.

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