def Lean.Meta.isConstructorApp? (e : Lean.Expr) : Lean.MetaM (Option Lean.ConstructorVal)

If e is a constructor application or a builtin literal defeq to a constructor application, then return the corresponding ConstructorVal.

Equations

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

def Lean.Meta.isConstructorApp'? (e : Lean.Expr) : Lean.MetaM (Option Lean.ConstructorVal)

Similar to isConstructorApp?, but uses whnf.

Equations

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

def Lean.Meta.isConstructorApp (e : Lean.Expr) : Lean.MetaM Bool

Returns true, if e is constructor application of builtin literal defeq to a constructor application.

Equations

• Lean.Meta.isConstructorApp e = do let __do_lift ← Lean.Meta.isConstructorApp? e pure (Option.isSome __do_lift)

def Lean.Meta.isConstructorApp' (e : Lean.Expr) : Lean.MetaM Bool

Returns true if isConstructorApp e or isConstructorApp (← whnf e)

Equations

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

def Lean.Meta.constructorApp? (e : Lean.Expr) : Lean.MetaM (Option (Lean.ConstructorVal × Array Lean.Expr))

If e is a constructor application, return a pair containing the corresponding ConstructorVal and the constructor application arguments.

Equations

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

def Lean.Meta.constructorApp'? (e : Lean.Expr) : Lean.MetaM (Option (Lean.ConstructorVal × Array Lean.Expr))

Similar to constructorApp?, but on failure it puts e in WHNF and tries again.

Equations

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