From 4bf2df563dae6490270db2fd48c66ca50b7e91b5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Oct 2022 07:05:44 -0700 Subject: [PATCH] fix: typo --- src/Lean/Compiler/LCNF/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index b94286f19e..757f10fb4b 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -686,13 +686,13 @@ where decls.forM fun decl => visit decl.value def instantiateRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array Arg) : Expr := - if !e.hasFVar then + if !e.hasLooseBVars then e else e.instantiateRange beginIdx endIdx (args.map (·.toExpr)) def instantiateRevRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array Arg) : Expr := - if !e.hasFVar then + if !e.hasLooseBVars then e else e.instantiateRevRange beginIdx endIdx (args.map (·.toExpr))