funProp
#
this file defines environment extension for funProp
Indicated origin of a function or a statement.
- decl: Lean.Name → Mathlib.Meta.FunProp.Origin
It is a constant defined in the environment.
- fvar: Lean.FVarId → Mathlib.Meta.FunProp.Origin
It is a free variable in the local context.
Instances For
Equations
- Mathlib.Meta.FunProp.instInhabitedOrigin = { default := Mathlib.Meta.FunProp.Origin.decl default }
Equations
Name of the origin.
Equations
- origin.name = match origin with | Mathlib.Meta.FunProp.Origin.decl name => name | Mathlib.Meta.FunProp.Origin.fvar id => id.name
Instances For
Get the expression specified by origin
.
Equations
- origin.getValue = match origin with | Mathlib.Meta.FunProp.Origin.decl name => Lean.Meta.mkConstWithFreshMVarLevels name | Mathlib.Meta.FunProp.Origin.fvar id => pure (Lean.Expr.fvar id)
Instances For
Pretty print FunProp.Origin
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty print FunProp.Origin
. Returns string unlike ppOrigin
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get origin of the head function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Default names to be considered reducible by fun_prop
Equations
- Mathlib.Meta.FunProp.defaultNamesToUnfold = #[`id, `Function.comp, `Function.HasUncurry.uncurry, `Function.uncurry]
Instances For
fun_prop
configuration
- constToUnfold : Batteries.RBSet Lean.Name Lean.Name.quickCmp
Name to unfold
- disch : Lean.Expr → Lean.MetaM (Option Lean.Expr)
Custom discharger to satisfy theorem hypotheses.
- maxDepth : ℕ
Maximal number of transitions between function properties e.g. inferring differentiability from linearity
- depth : ℕ
current depth
- thmStack : List Mathlib.Meta.FunProp.Origin
Stack of used theorem, used to prevent trivial loops.
- maxSteps : ℕ
Maximum number of steps
fun_prop
can take.
Instances For
Equations
- One or more equations did not get rendered due to their size.
fun_prop
state
- 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 - numSteps : ℕ
Count the number of steps and stop when maxSteps is reached.
Log progress and failures messages that should be displayed to the user at the end.
Instances For
Log used theorem
Equations
Instances For
Increase depth
Equations
Instances For
Equations
Instances For
Check if previously used theorem was thmOrigin
.
Equations
Instances For
Puts the theorem to the stack of used theorems.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Default names to unfold
Equations
Instances For
Get predicate on names indicating if theys shoulds be unfolded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Increase heartbeat, throws error when maxSteps
was reached
Equations
- One or more equations did not get rendered due to their size.
Instances For
Log error message that will displayed to the user at the end.
Equations
- Mathlib.Meta.FunProp.logError msg = modify fun (s : Mathlib.Meta.FunProp.State) => { cache := s.cache, numSteps := s.numSteps, msgLog := msg :: s.msgLog }