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

If e is a constructor application, then return the corresponding ConstructorVal.

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

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

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

Similar to isConstructorApp?, but uses whnf. It also uses isOffset? for Nat.

See also Lean.Meta.constructorApp'?.

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

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

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

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

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

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

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

Similar to constructorApp?, but on failure it puts e in WHNF and tries again. It also uses isOffset? for Nat.

See also Lean.Meta.isConstructorApp'?.