def Lean.Meta.Monotonicity.headBetaUnderLambda (f : Expr) : Expr

Equations

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

opaque Lean.Meta.Monotonicity.monotoneExt : SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name)

Environment extensions for monotonicity lemmas

def Lean.Meta.Monotonicity.findMonoThms (e : Expr) : MetaM (Array Name)

Finds tagged monotonicity theorems of the form monotone (fun x => e).

Equations

• Lean.Meta.Monotonicity.findMonoThms e = do let __do_lift ← Lean.getEnv (Lean.ScopedEnvExtension.getState Lean.Meta.Monotonicity.monotoneExt __do_lift).getMatch e

def Lean.Meta.Monotonicity.defaultFailK {α : Type} (f : Expr) (monoThms : Array Name) : MetaM α

Equations

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

partial def Lean.Meta.Monotonicity.solveMonoCall (α inst_α e : Expr) : MetaM (Option Expr)

Base case for solveMonoStep: Handles goals of the form

monotone (fun f => f.1.2 x y)

It's tricky to solve them compositionally from the outside in, so here we construct the proof from the inside out.

def Lean.Meta.Monotonicity.solveMonoStep (failK : {α : Type} → Expr → Array Name → MetaM α := @defaultFailK) (goal : MVarId) : MetaM (List MVarId)

Equations

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

partial def Lean.Meta.Monotonicity.solveMono (failK : {α : Type} → Expr → Array Name → MetaM α := fun {α : Type} => defaultFailK) (goal : MVarId) : MetaM Unit

def Lean.Meta.Monotonicity.evalMonotonicity : Elab.Tactic.Tactic

Equations

• Lean.Meta.Monotonicity.evalMonotonicity _stx = Lean.Elab.Tactic.liftMetaTactic Lean.Meta.Monotonicity.solveMonoStep