max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: missing argument

Browse source
This commit is contained in:
Leonardo de Moura 2021-07-23 11:37:28 -07:00
parent 1eee82f745
commit 1630cd3eb5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Closure.lean
View file

@ -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