source
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.

Instances For

source
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

Instances For

source
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.

Instances For

source
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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For