bug fix in splitHighOrderLambdaToComp

lecopivo · Sep 15, 2023 · c2bdcf2 · c2bdcf2
1 parent 9f6c75f
commit c2bdcf2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/SciLean/Lean/Meta/Basic.lean b/SciLean/Lean/Meta/Basic.lean
@@ -311,7 +311,7 @@ def splitHighOrderLambdaToComp (e : Expr) (mk := ``Prod.mk) (fst := ``Prod.fst)
         let yId ← withLCtx lctx instances mkFreshFVarId
         lctx := lctx.mkLocalDecl yId (name) yFVarType
         let yFVar := Expr.fvar yId
-        let yVal ← mkAppM' yFVar is'
+        let yVal := mkAppN yFVar is'
         yFVars := yFVars.push yFVar
         yVals := yVals.push yVal
         ys' := ys'.push f