@[inline]
Instances For
Instances For
def
Lean.Expr.constructorApp?
(env : Lean.Environment)
(e : Lean.Expr)
(useRaw : optParam Bool false)
:
If e is a constructor application, return a pair containing the corresponding ConstructorVal and the constructor
application arguments.
This function treats numerals as constructors. For example, if e is the numeral 2, the result pair
is ConstructorVal for Nat.succ, and the array #[1]. The parameter useRaw controls how the resulting
numeral is represented. If useRaw := false, then mkNatLit is used, otherwise mkRawNatLit.
Recall that mkNatLit uses the OfNat.ofNat application which is the canonical way of representing numerals
in the elaborator and tactic framework. We useRaw := false in the compiler (aka code generator).