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.

## Instances For

Similar to `isConstructorApp?`

, but uses `whnf`

.

## Equations

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

## Instances For

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)

## Instances For

Returns `true`

if `isConstructorApp e`

or `isConstructorApp (← whnf e)`

## Equations

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

## Instances For

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

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.