mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 10:41:59 +03:00
acd9c09a05
`p` was used for both the filter predicate and the length of the filtered vector. This renames the latter to n'. |
||
|---|---|---|
| .. | ||
| conclusions.rst | ||
| index.rst | ||
| interactive.rst | ||
| interfaces.rst | ||
| interp.rst | ||
| introduction.rst | ||
| miscellany.rst | ||
| modules.rst | ||
| multiplicities.rst | ||
| packages.rst | ||
| starting.rst | ||
| theorems.rst | ||
| typesfuns.rst | ||
| views.rst | ||
| windows.rst | ||