We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 60f3328 commit 106081eCopy full SHA for 106081e
src/Lean/Meta/Tactic/Apply.lean
@@ -241,8 +241,8 @@ def _root_.Lean.MVarId.applyN (mvarId : MVarId) (e : Expr) (n : Nat) (useApproxD
241
unless mvarIds.size == n do
242
throwError "Applied type takes fewer than {n} arguments:\n{indentExpr eType}"
243
unless (← isDefEqApply useApproxDefEq eType targetType) do
244
- throwError "Type mismatch: target is\n{indentExpr targetType}\nbut applied expression has \
245
- type\n{indentExpr eType}\nafter applying {n} arguments."
+ throwError "Type mismatch: target is{indentExpr targetType}\nbut applied expression has \
+ type{indentExpr eType}\nafter applying {n} arguments."
246
mvarId.assign (e.beta mvarIds)
247
return (mvarIds.map (·.mvarId!)).toList
248
0 commit comments