funProp

this file defines environment extension for funProp

structure Mathlib.Meta.FunProp.Config : Type

• constToUnfold : Lean.HashSet Lean.Name

  Name to unfold

• disch : Lean.Expr → Lean.MetaM (Option Lean.Expr)

  Custom discharger to satisfy theorem hypotheses.

• maxTransitionDepth : ℕ

  Maximal number of transitions between function properties e.g. inferring differentiability from linearity

• thmStack : List Lean.Meta.Origin

  Stack of used theorem, used to prevent trivial loops.

structure Mathlib.Meta.FunProp.State : Type

• cache : Lean.Meta.Simp.Cache

  Simp's cache is used as the funProp tactic is designed to be used inside of simp and utilize its cache

• transitionDepth : ℕ

  The number of used transition theorems.

def Mathlib.Meta.FunProp.Config.addThm (cfg : Mathlib.Meta.FunProp.Config) (thmId : Lean.Meta.Origin) : Mathlib.Meta.FunProp.Config

Log used theorem

Equations

• Mathlib.Meta.FunProp.Config.addThm cfg thmId = { constToUnfold := cfg.constToUnfold, disch := cfg.disch, maxTransitionDepth := cfg.maxTransitionDepth, thmStack := thmId :: cfg.thmStack }

@[inline, reducible]

abbrev Mathlib.Meta.FunProp.FunPropM (α : Type) : Type

Equations

• Mathlib.Meta.FunProp.FunPropM = ReaderT Mathlib.Meta.FunProp.Config (StateT Mathlib.Meta.FunProp.State Lean.MetaM)

structure Mathlib.Meta.FunProp.Result : Type

Result of funProp, it is a proof of function property P f

• proof : Lean.Expr

def Mathlib.Meta.FunProp.getLastUsedTheoremName : Mathlib.Meta.FunProp.FunPropM (Option Lean.Name)

Get the name of previously used theorem.

Equations

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