Now, even if the user opens the namespaces in the "wrong" order, the notation + coercions will behave as expected. |
||
|---|---|---|
| .. | ||
| basic.lean | ||
| complete.lean | ||
| default.lean | ||
| division.lean | ||
| order.lean | ||
| real.md | ||
Now, even if the user opens the namespaces in the "wrong" order, the notation + coercions will behave as expected. |
||
|---|---|---|
| .. | ||
| basic.lean | ||
| complete.lean | ||
| default.lean | ||
| division.lean | ||
| order.lean | ||
| real.md | ||