max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
16766 commits 1 branch 0 tags 5.3 GiB
Commit graph

3 commits

Author SHA1 Message Date
Leonardo de Moura
280e7bb006 feat(library/init/lean/attributes): add TagAttributes 
`TagAttribute`s are implemented on top of the low level Attribute API,
and `PersistentEnvExtension`.
This is just the first attribute on a series of attributes we are
going to implement using Lean itself.
 2019-06-05 21:54:28 -07:00
Leonardo de Moura
d212abb9ee feat(library/init/lean/syntax): export helper functions for creating syntax in C++ 2019-06-05 16:49:58 -07:00
Leonardo de Moura
7909d86e5d feat(library/init/lean): Syntax objects with new SyntaxNodeKind and Substring, and arrays instead of lists 
We can use `SyntaxNodeKind.id : Nat` to implement maps from kind to
values using arrays.
 2019-06-05 15:35:51 -07:00