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

fix: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-08 12:22:00 -07:00
parent 502758b09c
commit 783ca47d1f
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/Init/Lean/Elab/Binders.lean
View file

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