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.

source
def HigherCategoryTheory.hcat_disch :
Lean.ParserDescr

A tactic for discharging common goals in higher category theory proofs. This tactic first attempts reflexivity (for definitional equalities), then omega (for arithmetic goals on indices), and finally grind (for more complex goals involving equational reasoning).

TODO: This tactic is incomplete and highly inefficient.

Equations
Instances For