697f69020f
It is still broken since we apply attributes before we compile code. Recall that attributes such as `@[export]` and `@[extern]` must be applied before we compile code. On the other hand, any attribute `attrName` ``` @[attrName] def foo := ... ``` which creates auxiliary definitions that depend on `foo` must be applied AFTER we generate code for `foo`. Otherwise, we will fail to compile the auxiliary definition since we don't have code for `foo` yet. I will fix the issue above by allowing attributes to specify when they should be applied. I will start with only two options: before and after code compilation. In the future, we may need more options (e.g., before elaboration), but I don't see the need yet. cc @kha |
||
|---|---|---|
| .. | ||
| control | ||
| data | ||
| lean | ||
| coe.lean | ||
| core.lean | ||
| default.lean | ||
| env_ext.lean | ||
| fix.lean | ||
| init.md | ||
| io.lean | ||
| platform.lean | ||
| util.lean | ||
| wf.lean | ||