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

feat(library/init/lean/syntax): update preresolved field

Browse source 
The `Nat` is for handling the ambiguous `.` notation in Lean during
preresolution. Recall that `x.y` may represent a hierarchical name or
a "field access".
This commit is contained in:
Leonardo de Moura 2019-07-19 11:11:50 -07:00
parent 2ad33a23db
commit 76c27c9aa4
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/syntax.lean
View file

@ -34,7 +34,7 @@ inductive Syntax (α : Type := Unit)
| missing {} : Syntax
| node (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
| atom {} (info : Option SourceInfo) (val : String) : Syntax
| ident {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Name) : Syntax
| ident {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Nat × Name)) : Syntax
| other : α → Syntax
instance stxInh {α} : Inhabited (Syntax α) :=