Documentation

Mathlib.Tactic.Explode.Datatypes

Explode command: datatypes #

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

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

Instances For

    The row in the Fitch table.

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

    • line : Option Nat

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

    • depth : Nat

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

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

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

    • deps : List (Option Nat)

      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

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

      Equations
      • entry.line! = entry.line.get!
      Instances For

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

        Instances For

          Find a row where Entry.expr == e.

          Equations
          • es.find? e = es.s[e]?
          Instances For

            Length of our entries.

            Equations
            Instances For

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                • entries.addSynonym expr entry = { s := Std.HashMap.insert entries.s expr entry, l := entries.l }
                Instances For