Inf Wert automatisch gezwungen wird, nach dem Muster

Question

passende

Lassen Sie uns sagen, dass wir eine unendliche Liste haben:

data InfList : Type -> Type where 
    (::) : (value : elem) -> Inf (InfList elem) -> InfList elem 

Und wir wollen endlich viele ihrer Elemente haben:

getPrefix : (count : Nat) -> InfList a -> List a 
getPrefix Z _ = [] 
getPrefix (S k) (value :: xs) = value :: getPrefix k (?rest) 

Also, was bleibt:

a : Type 
    k : Nat 
    value : a 
    xs : InfList a 
-------------------------------------- 
rest : InfList a 

Es stellte sich heraus, dass nach Musterabgleich xs werden InfList a instea d von Inf (InfList a).

Gibt es eine Möglichkeit, xs verzögert zu haben?

Answer 1

Es scheint sich sowieso zu verzögern.

Wenn Sie :x getPrefix 10 one mit ausführen

one : InfList Int one = 1 :: one

Sie erhalten 1 :: getPrefix 9 (1 :: Delay one)

Ich kann es nicht mehr in der Dokumentation aber idris scheint Delay automatisch einzufügen.

Answer 2

Versuchen Sie einfach, Delay Konstruktor manuell hinzuzufügen. Es wird implizit entfernt.

getPrefix : (count : Nat) -> InfList a -> List a 
getPrefix Z _ = [] 
getPrefix (S k) (value :: Delay xs) = value :: getPrefix k xs