From 1630cd3eb59a939dcf86038dde812bf16f3bdcda Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Jul 2021 11:37:28 -0700 Subject: [PATCH] chore: missing argument --- src/Lean/Meta/Closure.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index cbc8622f8f..68a1b8facd 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -365,9 +365,9 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f return mkAppN (mkConst name result.levelArgs.toList) result.exprArgs /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/ -def mkAuxDefinitionFor (name : Name) (value : Expr) : MetaM Expr := do +def mkAuxDefinitionFor (name : Name) (value : Expr) (zeta : Bool := false) : MetaM Expr := do let type ← inferType value let type := type.headBeta - mkAuxDefinition name type value + mkAuxDefinition name type value (zeta := zeta) end Lean.Meta