From 3a08dd2771637b5f9759bc68027a5dfd833718ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Dec 2020 09:27:31 -0800 Subject: [PATCH] chore: typo --- src/Lean/Elab/Match.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 8afd75d7ae..b560a1c147 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -747,7 +747,7 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi | _ => pure () ``` If `synthesizeSyntheticMVarsNoPostponing`, the example above fails at `x.fst` because - the type of `x` is only available adfer we proces the last argument of `List.forM`. + the type of `x` is only available after we proces the last argument of `List.forM`. We apply pending default types to make sure we can process examples such as ```