Constant folding for primitives that have special runtime support.
Equations
- Lean.Compiler.getInfoFromFn fn [] = none
- Lean.Compiler.getInfoFromFn fn (info :: infos) = if (info.ofNatFn == fn) = true then some info else Lean.Compiler.getInfoFromFn fn infos
Instances For
Instances For
@[export lean_get_num_lit]
Equations
- Lean.Compiler.getNumLit (Lean.Expr.lit (Lean.Literal.natVal n)) = some n
- Lean.Compiler.getNumLit (Lean.Expr.app (Lean.Expr.const fn us) a) = if Lean.Compiler.isOfNat fn = true then Lean.Compiler.getNumLit a else none
- Lean.Compiler.getNumLit x = none