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

16 commits

Author SHA1 Message Date
Leonardo de Moura
82a36fbfe2 feat: declare_syntax_cat without importing Init.Lean 
cc @Kha
 2020-01-11 09:02:50 -08:00
Leonardo de Moura
e817257922 feat: elaborate declare_syntax_cat 
TODO: `registerParserCategory` uses `registerAttribute` which relies
on the environment having a declaration of type `AttributeImpl`.
This is bad since forces users to import `Init.Lean`.

@Kha The key problem is that we cannot serialize `AttributeImpl`.
I will try to address this issue tomorrow. I am considering different
workarounds.
 2020-01-10 21:10:02 -08:00
Leonardo de Moura
799914daf2 feat: registerParserCategory 2020-01-10 20:32:16 -08:00
Leonardo de Moura
3c8d8c7434 feat: add attributeExtension 2020-01-10 19:51:53 -08:00
Leonardo de Moura
48600dbbfc refactor: registerAttribute ==> registerBuiltinAttribute 2020-01-10 17:08:12 -08:00
Leonardo de Moura
fe09e99fef chore: disable attribute features that are not currently being used 2020-01-08 15:49:55 -08:00
Leonardo de Moura
0231841984 feat: applyAttributes 2020-01-05 16:22:46 -08:00
Leonardo de Moura
88339be110 refactor: improve initialization 2019-12-31 13:39:36 -08:00
Leonardo de Moura
b3d3d3c41a fix: initialization issue 2019-12-31 12:13:30 -08:00
Leonardo de Moura
76ec8fc843 chore: add TODO 2019-12-31 11:57:50 -08:00
Leonardo de Moura
d584f1b24e feat: add Environment as an extra parameter to addImportedFn 2019-12-31 11:11:37 -08:00
Leonardo de Moura
7057d71971 refactor: add new parameter to PersistentEnvExtension 2019-12-31 09:18:40 -08:00
Leonardo de Moura
067dca5a65 chore: naming convention 2019-12-15 18:28:00 -08:00
Leonardo de Moura
248cc2ec3a chore: naming convention 2019-12-15 07:48:42 -08:00
Leonardo de Moura
c3005671f5 chore: avoid ^do ... 2019-12-11 06:19:12 -08:00
Leonardo de Moura
c445199747 chore: library/Init ==> src/Init 
cc @Kha @dselsam @cipher1024
 2019-11-22 06:06:05 -08:00
Renamed from library/Init/Lean/Attributes.lean (Browse further)