def Lean.Meta.isConstructorAppCore? (e : Expr) : MetaM (Option 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 : Expr) : MetaM (Option 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 : Expr) : MetaM (Option ConstructorVal)

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

See also Lean.Meta.constructorApp'?.

Equations

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

def Lean.Meta.isConstructorApp (e : Expr) : 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 : Expr) : 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 : Expr) : MetaM (Option (ConstructorVal × Array 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 : 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'?.

Equations

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