# Explode command: datatypes #

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

source
inductive Mathlib.Explode.Status :
Type

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

- sintro : Status

  `├` Start intro (top-level)

- intro : Status

  `Entry.depth` * `│` + `┌` Normal intro

- cintro : Status

  `Entry.depth` * `│` + `├` Continuation intro

- lam : Status

  `Entry.depth` * `│`

- reg : Status

  `Entry.depth` * `│`

Instances For

source
def Mathlib.Explode.instInhabitedStatus.default :
Status
Equations

- Mathlib.Explode.instInhabitedStatus.default = Mathlib.Explode.Status.sintro

Instances For

source
instance Mathlib.Explode.instInhabitedStatus :
Inhabited Status
Equations

- Mathlib.Explode.instInhabitedStatus = { default := Mathlib.Explode.instInhabitedStatus.default }

source
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 Nat

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

- depth : Nat

  How many `if`s (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 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

source
def Mathlib.Explode.Entry.line! (entry : Entry) :
Nat

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

Equations

- entry.line! = entry.line.get!

Instances For

source
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 `Expr`s fast.

- l : List Entry

  Simple list of `Expr`s.

Instances For

source
def Mathlib.Explode.instInhabitedEntries.default :
Entries
Equations

- Mathlib.Explode.instInhabitedEntries.default = { s := default, l := default }

Instances For

source
instance Mathlib.Explode.instInhabitedEntries :
Inhabited Entries
Equations

- Mathlib.Explode.instInhabitedEntries = { default := Mathlib.Explode.instInhabitedEntries.default }

source
def Mathlib.Explode.Entries.find? (es : Entries) (e : Lean.Expr) :
Option Entry

Find a row where `Entry.expr` == `e`.

Equations

- es.find? e = es.s[e]?

Instances For

source
def Mathlib.Explode.Entries.size (es : Entries) :
Nat

Length of our entries.

Equations

- es.size = Std.HashMap.size es.s

Instances For

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

Equations

- entries.addSynonym expr entry = { s := Std.HashMap.insert entries.s expr entry, l := entries.l }

Instances For