FStarLang / FStarLang/fstarlang.github.io
Definition on `length` incorrect in one spot
Open
- Dominant language
- HTML
- Stars
- 8
- Forks
- 9
- PR merge metrics
- No merged PRs in 30d
Description
At this line in the docs:
https://github.com/FStarLang/fstarlang.github.io/blob/6a01e34c2db37759bd192934429bb8f83fc0b993/book/html/part1/part1_termination.html#L269
The recursive definition of `length` is missing the `1 + ...` that is present in the previous definition here:
https://github.com/FStarLang/fstarlang.github.io/blob/6a01e34c2db37759bd192934429bb8f83fc0b993/book/html/part1/part1_termination.html#L259
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.