Documentation

Lean.Meta.AbstractNestedProofs

def Lean.Meta.AbstractNestedProofs.isNonTrivialProof (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.AbstractNestedProofs.isNonTrivialProof e = do let a ← Lean.Meta.isProof e if (!a) = true then pure false else Lean.Expr.withApp e fun f args => pure (!Lean.Expr.isAtomic f || Array.any args (fun arg => !Lean.Expr.isAtomic arg) 0 (Array.size args))

structure Lean.Meta.AbstractNestedProofs.Context :

Type

baseName : Lean.Name

structure Lean.Meta.AbstractNestedProofs.State :

Type

nextIdx : Nat

@[inline]

abbrev Lean.Meta.AbstractNestedProofs.M (α : Type) :

Type

Equations

Lean.Meta.AbstractNestedProofs.M = ReaderT Lean.Meta.AbstractNestedProofs.Context (Lean.MonadCacheT Lean.ExprStructEq Lean.Expr (StateRefT' IO.RealWorld Lean.Meta.AbstractNestedProofs.State Lean.MetaM))

partial def Lean.Meta.AbstractNestedProofs.visit (e : Lean.Expr) :

Lean.Meta.AbstractNestedProofs.M Lean.Expr

def Lean.Meta.abstractNestedProofs (mainDeclName : Lean.Name) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.abstractNestedProofs mainDeclName e = StateRefT'.run' (Lean.MonadCacheT.run (ReaderT.run (Lean.Meta.AbstractNestedProofs.visit e) { baseName := mainDeclName })) { nextIdx := 1 }