`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. |
||
|---|---|---|
| .. | ||
| control | ||
| data | ||
| lean | ||
| coe.lean | ||
| core.lean | ||
| default.lean | ||
| env_ext.lean | ||
| fix.lean | ||
| init.md | ||
| io.lean | ||
| platform.lean | ||
| util.lean | ||
| wf.lean | ||