mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-23 03:05:00 +03:00
c75569c255
Slight change of plan: instead of having special names, add Lazy, Inf, Delay and Force and keywords and elaborate them specially. Correspondingly, add DelayCase for case trees. Given that implicit laziness is important, it seems better to do it this way than constantly check whether the name we're working with is important. This turns out to make implicit laziness much easier, because the unifier can flag whether it had to go under a 'Delayed' to succeed, and report that back to the elaborator which can then insert the necessary coercion.
5 lines
69 B
Plaintext
5 lines
69 B
Plaintext
ones
|
|
take (S (S (S Z))) ones
|
|
every2nd (S (S (S Z))) (countFrom 1)
|
|
:q
|