← Copula mathematical handbook

Discrimination-tree-indexed environment extensions

This file provides an API for scoped environment extensions whose declarations are indexed by elaborated expression patterns in a DiscrTree.

Implimentation Notes

The inclusion tactic uses two seperate types of DiscrTree indexed environment extensions. These have nearly identical APIs except the stored values are different types (one is InclusionExts and the other is HypothesisExts). This file essentially generalizes the DiscrTree valued environment extension API from the implimentation for the norm_num tactic so that it can take arbitrary values.

TODO

Investigate the possibility of using this API for other tactics in Mathlib with DiscrTree indexed environment extensions such as norm_num and positivity. This should perhaps be part of a wider investigation into whether more API from the environment extensions of various Mathlib tactics could be unified.

def DiscrTreeExt.evalDecl (α : Type) (typeName declName : Lean.Name) : Lean.ImportM α

Evaluate declName as a value of type α, checking that its Lean type is typeName.

Equations

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

@[reducible, inline]

abbrev DiscrTreeExt.Entry : Type

The discrimination-tree paths and declaration name stored in an .olean entry.

Equations

• DiscrTreeExt.Entry = (Array (Array Lean.Meta.DiscrTree.Key) × Lean.Name)

structure DiscrTreeExt.State (α : Type) : Type

The state of a discrimination-tree environment extension.

• tree : Lean.Meta.DiscrTree α

  The discrimination tree of the extension.

@[instance_reducible]

instance DiscrTreeExt.instInhabitedState {a✝ : Type} : Inhabited (State a✝)

Equations

• DiscrTreeExt.instInhabitedState = { default := DiscrTreeExt.instInhabitedState.default }

@[reducible, inline]

abbrev DiscrTreeExt.EnvExt (α : Type) : Type

A scoped environment extension containing declaration values indexed by expression patterns.

Equations

• DiscrTreeExt.EnvExt α = Lean.ScopedEnvExtension DiscrTreeExt.Entry (DiscrTreeExt.Entry × α) (DiscrTreeExt.State α)

def DiscrTreeExt.State.getMatch {α : Type} (state : State α) (e : Lean.Expr) : Lean.MetaM (Array α)

Return the declaration values whose DiscrTree keys match e.

Equations

• state.getMatch e = state.tree.getMatch e

def DiscrTreeExt.initializeEnvExt {α : Type} (typeName : Lean.Name) (envExtName : Lean.Name := by exact decl_name%) : IO (EnvExt α)

Create a scoped environment extension whose declarations have type typeName. By default, the environment extension is named after the declaration in which this function is called.

Equations

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

def DiscrTreeExt.elabExtKeys (patterns : Array Lean.Syntax) : Lean.CoreM (Array (Array Lean.Meta.DiscrTree.Key))

Elaborate expression patterns into DiscrTree paths.

Equations

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