371392 (9) [Avatar] Offline
#1
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
447389 (1) [Avatar] Offline
#2
Really thank you for your great post.Recently i searched for this topic but i dont get it.Now i am really happy to see your article.I have website based on honda jazz price in kasaragod .This article is help me to solve some technical issues in my website.thanks for your great job.