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

Equations

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

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

Environment extensions for monotonicity lemmas

def Lean.Meta.Monotonicity.findMonoThms (e : Lean.Expr) : Lean.MetaM (Array Lean.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

partial def Lean.Meta.Monotonicity.solveMonoCall (α inst_α e : Lean.Expr) : Lean.MetaM (Option Lean.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} → Lean.Expr → Array Lean.Name → Lean.MetaM α := @Lean.Meta.Monotonicity.defaultFailK✝) (goal : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Equations

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

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

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

Equations

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