From f61ec4929fbc4c0a1e37263eb4a22b277309ec08 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Oct 2022 12:01:33 -0700 Subject: [PATCH] chore: add low-level `normExprCore` --- src/Lean/Compiler/LCNF/CompilerM.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean index 534f65111b..2cb6887bbe 100644 --- a/src/Lean/Compiler/LCNF/CompilerM.lean +++ b/src/Lean/Compiler/LCNF/CompilerM.lean @@ -239,6 +239,10 @@ See `Check.lean` for the free variable substitution checker. @[inline, inheritDoc normExprImp] def normExpr [MonadFVarSubst m t] [Monad m] (e : Expr) : m Expr := return normExprImp (← getSubst) e t +@[inheritDoc normExprImp] +abbrev normExprCore (s : FVarSubst) (e : Expr) (translator : Bool) : Expr := + normExprImp s e translator + /-- Normalize the given expressions using the current substitution. -/