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