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
    • 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.

    The row in the Fitch table.

    Instances For

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

      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.

          Instances For

            Length of our entries.

            Instances For

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

              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.

                Instances For