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

fix: Syntax.setHeadInfo

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-15 14:39:40 +02:00
parent ed326491ab
commit e83edefcc1
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Lean/Syntax.lean
View file

@ -233,9 +233,9 @@ partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
| atom _ val => some $ atom info val
| ident _ rawVal val pre => some $ ident info rawVal val pre
| node k args =>
match updateFirst args setHeadInfoAux args.size with
match updateFirst args setHeadInfoAux 0 with
| some args => some $ node k args
| noxne => none
| noxne => none
| stx => none
def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=