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

chore(library/init/lean/parser/term): remove hack used during conversion

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-21 09:51:05 -07:00
parent fc40fbb93f
commit 930164b597
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/lean/parser/term.lean
View file

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