From 0196bca784f82f90b4efd2a85a400daf4ab767f8 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Thu, 26 Sep 2024 06:51:23 +0200 Subject: [PATCH] doc: fix typo in docstring of `computeSynthOrder` (#5398) --- src/Lean/Meta/Instances.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 73daaa508d..0898873199 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -101,7 +101,7 @@ private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do DiscrTree.mkPath type tcDtConfig /-- -Compute the order the arguments of `inst` should by synthesized. +Compute the order the arguments of `inst` should be synthesized. The synthesization order makes sure that all mvars in non-out-params of the subgoals are assigned before we try to synthesize it. Otherwise it goes left