From 783ca47d1fde2750af8ef765ead86dcd3120009f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Mar 2020 12:22:00 -0700
Subject: [PATCH] fix: typo

---
 src/Init/Lean/Elab/Binders.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Elab/Binders.lean b/src/Init/Lean/Elab/Binders.lean
index f671e5e86c..219a605723 100644
--- a/src/Init/Lean/Elab/Binders.lean
+++ b/src/Init/Lean/Elab/Binders.lean
@@ -163,7 +163,7 @@ else do
     x fvars
 
 @[inline] def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α :=
-elabBinders #[binder] (fun fvars => x (fvars.get! 1))
+elabBinders #[binder] (fun fvars => x (fvars.get! 0))
 
 @[builtinTermElab «forall»] def elabForall : TermElab :=
 fun stx _ => match_syntax stx with