From 930164b59784b37c8bc5d32a382c935306146fc2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Mar 2019 09:51:05 -0700 Subject: [PATCH] chore(library/init/lean/parser/term): remove hack used during conversion --- library/init/lean/parser/term.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index c52a2be19a..0967226099 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -96,10 +96,10 @@ nodeChoice! simpleBinder { } def simpleBinder.View.toBinderInfo : simpleBinder.View → (BinderInfo × SyntaxIdent × Syntax) -| (simpleBinder.View.explicit {id := id, type := type, ..}) := (BinderInfo.default, id, type) -| (simpleBinder.View.implicit {id := id, type := type, ..}) := (BinderInfo.implicit, id, type) -| (simpleBinder.View.strictImplicit {id := id, type := type, ..}) := (BinderInfo.strictImplicit, id, type) -| (simpleBinder.View.instImplicit {id := id, type := type, ..}) := (BinderInfo.instImplicit, id, type) +| (simpleBinder.View.explicit {id := id, type := type}) := (BinderInfo.default, id, type) +| (simpleBinder.View.implicit {id := id, type := type}) := (BinderInfo.implicit, id, type) +| (simpleBinder.View.strictImplicit {id := id, type := type}) := (BinderInfo.strictImplicit, id, type) +| (simpleBinder.View.instImplicit {id := id, type := type}) := (BinderInfo.instImplicit, id, type) @[derive Parser.HasTokens Parser.HasView] def anonymousConstructor.Parser : termParser :=