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
                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
                          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
                              Instances For