@[reducible, inline]
Equations
Instances For
@[irreducible]
def
Lean.Compiler.LCNF.ToExpr.mkLambdaM.go
(params : Array Param)
(offset : Nat)
(m : Lean.Compiler.LCNF.ToExpr.LevelMap✝)
(i : Nat)
(e : Expr)
:
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[inline]
def
Lean.Compiler.LCNF.ToExpr.run
{α : Type}
(x : ToExprM α)
(offset : Nat := 0)
(levelMap : Lean.Compiler.LCNF.ToExpr.LevelMap✝ := ∅)
:
α