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

doc: TSyntax

Browse source
This commit is contained in:
Sebastian Ullrich 2022-06-24 23:33:33 +02:00
parent 8b4d8b8dc9
commit e47f248161
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Prelude.lean
View file

@ -1847,6 +1847,12 @@ inductive Syntax where
def SyntaxNodeKinds := List SyntaxNodeKind
/--
A `Syntax` value of one of the given syntax kinds.
Note that while syntax quotations produce/expect `TSyntax` values of the correct kinds,
this is not otherwise enforced and can easily be circumvented by direct use of the constructor.
The namespace `TSyntax.Compat` can be opened to expose a general coercion from `Syntax` to any
`TSyntax ks` for porting older code. -/
structure TSyntax (ks : SyntaxNodeKinds) where
raw : Syntax
@ -1989,6 +1995,7 @@ partial def getTailPos? (stx : Syntax) (originalOnly := false) : Option String.P
structure SepArray (sep : String) where
elemsAndSeps : Array Syntax
/-- A typed version of `SepArray`. -/
structure TSepArray (ks : SyntaxNodeKinds) (sep : String) where
elemsAndSeps : Array Syntax