Agda list question Change the denition of listprefixes in ht

Agda list question:

Change the denition of list-prefixes in html.agda so that it takes in an input list l and returns a list of all the prexes of l, from shortest to longest. A prex of a list l is a list that begins l. Just consider nonempty prexes. The entire list will be considered a prex of itself. For example is and code is: list prefixes Forall {A: Set} rightarrow LA rightarrow L (LA) list-prefixes l = {!!} can someone explain what should i go to solve the problem? My thought is to remove the tail one by one, and reverse them. but i don\'t know how to do it.

Solution

module _ {} {A : Set } > where > data Null : List A Set where isNull : Null [] > > null? : (xs : List A) Dec (Null xs) > null? [] = yes isNull > null? (_ _) = no () > > -------------------------------------------------------- > f : List > f [] = 1 > f (_ _) = 0 > > postulate ps : List > > g : Dec (f ps 1) > g with null? ps > ... | yes null-ps = yes (h null-ps) > ... | no _ = no neq > where > postulate neq : f ps 1 > > g\' : Dec (f ps 1) > g\' > with ps | null? ps > ... | _ | yes null-ps = yes (h null-ps) > ... | _ | no _ = no neq > where > postulate neq : f ps 1 > -------------------------------------------------------------------- > > g is type-checked, > and for g\' it reports that null-ps has not the needed > type. > > (The Agda language is difficult in its proof composition part. > I do not understand basics of Agda after 3 year practicing > with it). > > In this example, the part \"ps |\" is dummy. > But in the real example I need to use both ps and null? ps, > like this: > > ... | [] | null-ps = foo null-ps > ... | (_ , 0) :: _ | _ = \\bot-elim ... 0>0 > ... > > g\' is a simplification for this real example.