Skip to content

Commit 196c6ae

Browse files
nomeataeric-wieser
andauthored
Update src/Lean/Meta/Closure.lean
Co-authored-by: Eric Wieser <[email protected]>
1 parent 2cf8794 commit 196c6ae

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Meta/Closure.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -357,7 +357,7 @@ private structure TopoSort where
357357
newArgs : Array Expr := #[]
358358

359359
/--
360-
By constrction, the `newLocalDecls` for fvars are in dependency order, but those for MVars may not be,
360+
By construction, the `newLocalDecls` for fvars are in dependency order, but those for MVars may not be,
361361
and need to be interleaved appropriately. This we do a “topological insertion sort” of these.
362362
We care about efficiency for the common case of many fvars and no mvars.
363363
-/

0 commit comments

Comments
 (0)