In the implementation for getPrefix in section 11.1.4 in step 4, you show the following hole:
a : Type
k : Nat
value : a
xs : Inf (InfList a)
--------------------------------------
getPrefix_rhs_1 : List a
… and finish the implementation with the clause
getPrefix (S k) (value :: xs) = value :: getPrefix k (Force xs)
However, this is not what I'm seeing in Idris 0.99. The Inf has already been removed and I don't need a Force:
- + Main.getPrefix_rhs_1 [P]
`-- a : Type
k : Nat
value : a
xs : InfList a
----------------------------------
Main.getPrefix_rhs_1 : List a
The next section talks about how Idris will implicitly insert Delay and Force for you. Has any of this behaviour changed between 0.12 and 0.99?
Here's the complete code:
data InfList : Type -> Type where
(::) : (value : elem) -> Inf (InfList elem) -> InfList elem
%name InfList xs, ys, zs
countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))
getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z _ = []
getPrefix (S k) (value :: xs) = ?getPrefix_rhs_1
|