Documentation

HigherCategoryTheory.Tactic

Proof automation for higher category theory #

This file provides the hcat_disch tactic, a proof automation tool for discharging common goals in higher category theory proofs. It is used extensively as the default proof method for most of the definitions of the library.

The hcat_disch tactic first tries a simple set of tactics and if those fail, it falls back to aesop_hcat, a wrapper around Aesop with the HigherCategoryTheory rule set.

source
def HigherCategoryTheory.aesop_hcat :
Lean.ParserDescr

A wrapper around Aesop for the HigherCategoryTheory rule set.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HigherCategoryTheory.aesop_hcat? :
    Lean.ParserDescr

    A suggestive version of aesop_hcat that produces a "Try this" suggestion on success.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def HigherCategoryTheory.hcat_disch :
      Lean.ParserDescr

      A tactic for discharging common goals in higher category theory proofs.

      Equations
      Instances For
        source
        def HigherCategoryTheory.hcat_disch? :
        Lean.ParserDescr

        A suggestive version of hcat_disch that produces a "Try this" suggestion on success.

        Equations
        Instances For