Documentation

Mathlib.Tactic.Order.CollectFacts

Facts collection for the order Tactic #

This file implements the collection of facts for the order tactic.

A structure for storing facts about variables.

Instances For
    @[reducible, inline]

    State for CollectFactsM. It contains a map where the key t maps to a pair (atomToIdx, facts). atomToIdx is a DiscrTree containing atomic expressions with their indices, and facts stores AtomicFacts about them.

    Equations
      Instances For
        @[reducible, inline]

        Monad for the fact collection procedure.

        Equations
          Instances For
            def Mathlib.Tactic.Order.addAtom {u : Lean.Level} (type : Q(Type u)) (x : Q(«$type»)) :

            Updates the state with the atom x.

            Equations
              Instances For

                Adds fact to the state.

                Equations
                  Instances For

                    Implementation for collectFacts in CollectFactsM monad.

                    Equations
                      Instances For

                        Extracts facts and atoms from the expression.

                        Equations
                          Instances For

                            Collects facts from the local context. For each occurring type α, the returned map contains a pair (idxToAtom, facts), where the map idxToAtom converts indices to found atomic expressions of type α, and facts contains all collected AtomicFacts about them.

                            Equations
                              Instances For