<div dir="ltr"><div style="min-height:100%"><div class="" style="width:1374.55px"><div class=""><div class=""><div class=""><div class="" style="width:1172.53px"><div class=""><div class=""><div class=""><div class=""><div id=":4" class="" style="height:584px"><div id=":2" class="" style="min-height:156.835px"><div class=""><div class=""><div class=""><table class="" cellpadding="0" style="width:1142.73px"><tbody><tr><td class=""><div class=""><div class=""><div class=""><div class=""><div class="" tabindex="-1"><div class="" style="width:883.821px"><div class=""><div id=":7n"><div class=""><div class=""><div id=":7p" class="" style="font-size:12.8px"><div id=":7o" class="" style="overflow:hidden"><div bgcolor="#FFFFFF" text="#000000"><div class=""><div class="im"><blockquote type="cite" style="font-size:12.8px"><div dir="ltr"><div>{--</div><div>   Hello guys, I am trying to gather many proofs using Agda now that I am studying it on own. </div><div>Bellow, I have a few problems I would love your help of solving. Thank you in advances guys.</div><div><br></div><div><br></div><div><br></div><div><br></div><div>--}</div><div>module list-todo where</div><div><br></div><div>open import lib</div><div><br></div><div>{- define this function so that it removes the last element from a list.</div><div>   If the list is empty, you can just return the empty list. -}</div><div>removelast : ∀{ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A</div><div>removelast = {!!}</div><div><br></div><div>{- once you have a correct definition of removelast, the yellow highlighting</div><div>   for the following two tests will disappear. -}</div><div>test1-removelast : removelast (1 :: 2 :: 3 :: 4 :: []) ≡ 1 :: 2 :: 3 :: []</div><div>test1-removelast = refl</div><div><br></div><div>test2-removelast : removelast (&#39;a&#39; :: &#39;b&#39; :: &#39;z&#39; :: &#39;y&#39; :: &#39;z&#39; :: []) ≡ &#39;a&#39; :: &#39;b&#39; :: &#39;z&#39; :: &#39;y&#39; :: []</div><div>test2-removelast = refl</div><div><br></div><div>concat[] : ∀ {ℓ}{A : Set ℓ}(n : ℕ) → concat{A = A} (repeat n []) ≡ []</div><div>concat[] = {!!}</div><div><br></div><div>-- you have to implement removelast above in order to do this problem</div><div>removelast++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → is-empty l2 ≡ ff → removelast (l1 ++ l2) ≡ l1 ++ removelast l2</div><div>removelast++ = {!!}</div><div><br></div><div>shorter-trans : ∀{ℓ}{A : Set ℓ}(l1 l2 l3 : 𝕃 A) → </div><div>                 l1 shorter l2 ≡ tt →</div><div>                 l2 shorter l3 ≡ tt →</div><div>                 l1 shorter l3 ≡ tt </div><div>shorter-trans = {!!}</div><div><br></div><div>list-all-any : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) → </div><div>                list-all pred l ≡ ~ (list-any (λ a → ~ (pred a)) l)</div><div>list-all-any = {!!}</div><div><br></div><div>filter-list-all : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) → </div><div>                   list-all pred l ≡ tt → </div><div>                   filter pred l ≡ l</div><div>filter-list-all = {!!}</div><div><br></div><div>filter-member : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(pred : A → 𝔹)(l : 𝕃 A) → </div><div>                list-member eq a (filter pred l) ≡ tt →</div><div>                list-member eq a l ≡ tt ∧ pred a ≡ tt</div><div>filter-member = {!!}</div><div><br></div><div><br></div><div>zip-unzip : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂}(x : 𝕃 A)(y : 𝕃 B) → </div><div>            length x ≡ length y → unzip (zip x y) ≡ x , y</div><div>zip-unzip = {!!} </div></div></blockquote><div><div dir="ltr"><div><br></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></td></tr></tbody></table></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>