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

If e is 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)

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

Equations

• Lean.Meta.isConstructorApp? e = do let __do_lift ← Lean.Meta.litToCtor e Lean.Meta.isConstructorAppCore? __do_lift

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 __do_lift.isSome

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. It also isOffset?

Equations

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