@kha we are currently avoiding `_` in file names. I am not super happy with names such as `neverextractattr.lean`. I am open to a new name convention for .lean files in the stdlib. |
||
|---|---|---|
| .. | ||
| basic.lean | ||
| basicaux.lean | ||
| default.lean | ||
| instances.lean | ||
@kha we are currently avoiding `_` in file names. I am not super happy with names such as `neverextractattr.lean`. I am open to a new name convention for .lean files in the stdlib. |
||
|---|---|---|
| .. | ||
| basic.lean | ||
| basicaux.lean | ||
| default.lean | ||
| instances.lean | ||