Refactor the lazy keywords to be actual keywords

[CodingCellist]

• [x] I have read CONTRIBUTING.md.
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

Prompted by a question from locria/locriacyber and spotted by gallais, the keywords for lazy things (e.g. Inf and Lazy) are actually not keywords but magic strings in the parser! This means we cannot do nice things like output :doc for them, leading to confusion for what they mean.

The immediately relevant parts seem to be:

• https://github.com/idris-lang/Idris2/blob/main/src/Idris/Parser.idr#L922-L935=
• https://github.com/idris-lang/Idris2/blob/main/src/TTImp/Parser.idr#L438-L459=

Although there'll probably be other bits that need changing as well.

Motivation

:doc support and having keywords be properly+consistently marked as such.

[iacore]

Is it a good idea to change Lazy a to () -> a and add syntax magic on it? Totality checker seem to work.

data LazyList : Type -> Type where
    Nil : LazyList a
    (::) : a -> (Unit -> LazyList a) -> LazyList a

total
all42 : LazyList Nat
all42 = 42 :: (\_ => all42)

1/1: Building reclazy (reclazy.idr)
Error: all42 is not total, possibly not terminating due to recursive path Main.all42 -> Main.all42

reclazy:5:1--6:21
 5 | total
 6 | all42 : LazyList Nat

Error(s) building file reclazy.idr

[iacore]

There is also Delay, which is kind of like runtime hint?

Main> :let d = \_ => delay 3
Main> d
\_ => Delay 3

[CodingCellist]

Will actually be closed if we merge #2992. Although #2987 adds :doc-support, it doesn't refactor the laziness primitives to be reserved (which is what the later PR does).

[CodingCellist]

Closing this as there seems to be opposition to #2992 , and all I mostly cared about was :doc support. If we discover that we absolutely need the keywords to be reserved, or someone has a strong case for it, feel free to reopen and have a look at #2992 : )