Documentation

Mathlib.Tactic.Explode.Datatypes

Explode command: datatypes #

This file contains datatypes used by the #explode command and their associated methods.

source
🔶 coverage
inductive Mathlib.Explode.Status :
Type

How to display pipes (│) for this entry in the Fitch table .

Instances For
    source
    🔸 coverage
    def Mathlib.Explode.instInhabitedStatus.default :
    Status
    Instances For
      source
      🔸 coverage
      @[implicit_reducible]
      instance Mathlib.Explode.instInhabitedStatus :
      Inhabited Status
      source
      🔶 coverage
      structure Mathlib.Explode.Entry :
      Type

      The row in the Fitch table.

      • type : Lean.MessageData

        A type of this expression as a MessageData. Make sure to use addMessageContext.

      • line : Option â„•

        The row number, starting from 0. This is set by Entries.add.

      • depth : â„•

        How many ifs (aka lambda-abstractions) this row is nested under.

      • status : Status

        What Status this entry has - this only affects how │s are displayed.

      • thm : Lean.MessageData

        What to display in the "theorem applied" column. Make sure to use addMessageContext if needed.

      • deps : List (Option â„•)

        Which other lines (aka rows) this row depends on. none means that the dependency has been filtered out of the table.

      • useAsDep : Bool

        Whether or not to use this in future deps lists. Generally controlled by the select function passed to explodeCore. Exception: ∀I may ignore this for introduced hypotheses.

      Instances For
        source
        🔸 coverage
        def Mathlib.Explode.Entry.line! (entry : Entry) :
        â„•

        Get the line for an Entry that has been added to the Entries structure.

        Instances For
          source
          🔶 coverage
          structure Mathlib.Explode.Entries :
          Type

          Instead of simply keeping a list of entries (List Entry), we create a datatype Entries that allows us to compare expressions faster.

          • s : Lean.ExprMap Entry

            Allows us to compare Exprs fast.

          • l : List Entry

            Simple list of Exprs.

          Instances For
            source
            🔸 coverage
            @[implicit_reducible]
            instance Mathlib.Explode.instInhabitedEntries :
            Inhabited Entries
            source
            🔸 coverage
            def Mathlib.Explode.instInhabitedEntries.default :
            Entries
            Instances For
              source
              🔸 coverage
              def Mathlib.Explode.Entries.find? (es : Entries) (e : Lean.Expr) :
              Option Entry

              Find a row where Entry.expr == e.

              Instances For
                source
                🔸 coverage
                def Mathlib.Explode.Entries.size (es : Entries) :
                â„•

                Length of our entries.

                Instances For
                  source
                  🔸 coverage
                  def Mathlib.Explode.Entries.add (entries : Entries) (expr : Lean.Expr) (entry : Entry) :
                  Entry × Entries

                  Add the entry unless it already exists. Sets the line field to the next available value.

                  Instances For
                    source
                    🔸 coverage
                    def Mathlib.Explode.Entries.addSynonym (entries : Entries) (expr : Lean.Expr) (entry : Entry) :
                    Entries

                    Add a pre-existing entry to the ExprMap for an additional expression. This is used by let bindings where expr is an fvar.

                    Instances For