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

doc: fix typo in docstring of computeSynthOrder (#5398)

Browse source
This commit is contained in:
Johan Commelin 2024-09-26 06:51:23 +02:00 • committed by GitHub
parent b320dcfef9
commit 0196bca784
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Instances.lean
View file

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