Explode command: datatypes

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

inductive Mathlib.Explode.Status : Type

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

• sintro: Mathlib.Explode.Status

  ├ Start intro (top-level)

• intro: Mathlib.Explode.Status

  Entry.depth * │ + ┌ Normal intro

• cintro: Mathlib.Explode.Status

  Entry.depth * │ + ├ Continuation intro

• lam: Mathlib.Explode.Status

  Entry.depth * │

• reg: Mathlib.Explode.Status

  Entry.depth * │

instance Mathlib.Explode.instInhabitedStatus : Inhabited Mathlib.Explode.Status

Equations

• Mathlib.Explode.instInhabitedStatus = { default := Mathlib.Explode.Status.sintro }

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 ifs (aka lambda-abstractions) this row is nested under.

• status : Mathlib.Explode.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.

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

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

Equations

• entry.line! = entry.line.get!

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 Mathlib.Explode.Entry

  Allows us to compare Exprs fast.

• l : List Mathlib.Explode.Entry

  Simple list of Exprs.

instance Mathlib.Explode.instInhabitedEntries : Inhabited Mathlib.Explode.Entries

Equations

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

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

Find a row where Entry.expr == e.

Equations

• es.find? e = Lean.HashMap.find? es.s e

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

Length of our entries.

Equations

• es.size = Lean.HashMap.size es.s

def Mathlib.Explode.Entries.add (entries : Mathlib.Explode.Entries) (expr : Lean.Expr) (entry : Mathlib.Explode.Entry) : Mathlib.Explode.Entry × Mathlib.Explode.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.

def Mathlib.Explode.Entries.addSynonym (entries : Mathlib.Explode.Entries) (expr : Lean.Expr) (entry : Mathlib.Explode.Entry) : Mathlib.Explode.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 := Lean.HashMap.insert entries.s expr entry, l := entries.l }