No help with homework on this list [Re: [Agda] Agda Questions.]

[Harley Eades III]

Hi, Andreas.

I see this a lot too.  I completely agree that we shouldn’t do things like this here.  

Homework is better served if it is down through the sweat and tears of the
students.  :-P

Very best,
Harley

> On Sep 22, 2015, at 8:11 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 
> I see this happening on the Coq list, "helpful" experts answering homework Coq assignments.  I think we should abstain from this here.
> 
> --Andreas
> 
> On 22.09.2015 14:02, Aaron Stump wrote:
>> Dear Agda list,
>> 
>> Yes, this is homework for my class, so thanks for your nonresponse.
>> 
>> Aaron
>> 
>> On Tue, Sep 22, 2015 at 6:32 AM, Andreas Abel <andreas.abel at ifi.lmu.de
>> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>> 
>>    Sounds like you want us to solve your homework. ;) --Andreas
>> 
>> 
>>    On 20.09.2015 23:36, Ismail Alyassiri wrote:
>> 
>>            {--
>>                Hello guys, I am trying to gather many proofs using Agda
>>            now that I
>>            am studying it on own.
>>            Bellow, I have a few problems I would love your help of
>>            solving. Thank
>>            you in advances guys.
>> 
>> 
>> 
>> 
>>            --}
>>            module list-todo where
>> 
>>            open import lib
>> 
>>            {- define this function so that it removes the last element
>>            from a list.
>>                If the list is empty, you can just return the empty list. -}
>>            removelast : ∀{ℓ}{A : Set ℓ} → 𝕃 A → 𝕃 A
>>            removelast = {!!}
>> 
>>            {- once you have a correct definition of removelast, the yellow
>>            highlighting
>>                for the following two tests will disappear. -}
>>            test1-removelast : removelast (1 :: 2 :: 3 :: 4 :: []) ≡ 1
>>            :: 2 :: 3 :: []
>>            test1-removelast = refl
>> 
>>            test2-removelast : removelast ('a' :: 'b' :: 'z' :: 'y' ::
>>            'z' :: [])
>>            ≡ 'a' :: 'b' :: 'z' :: 'y' :: []
>>            test2-removelast = refl
>> 
>>            concat[] : ∀ {ℓ}{A : Set ℓ}(n : ℕ) → concat{A = A} (repeat n
>>            []) ≡ []
>>            concat[] = {!!}
>> 
>>            -- you have to implement removelast above in order to do
>>            this problem
>>            removelast++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → is-empty l2 ≡
>>            ff →
>>            removelast (l1 ++ l2) ≡ l1 ++ removelast l2
>>            removelast++ = {!!}
>> 
>>            shorter-trans : ∀{ℓ}{A : Set ℓ}(l1 l2 l3 : 𝕃 A) →
>>                              l1 shorter l2 ≡ tt →
>>                              l2 shorter l3 ≡ tt →
>>                              l1 shorter l3 ≡ tt
>>            shorter-trans = {!!}
>> 
>>            list-all-any : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) →
>>                             list-all pred l ≡ ~ (list-any (λ a → ~
>>            (pred a)) l)
>>            list-all-any = {!!}
>> 
>>            filter-list-all : ∀{ℓ}{A : Set ℓ}(pred : A → 𝔹)(l : 𝕃 A) →
>>                                list-all pred l ≡ tt →
>>                                filter pred l ≡ l
>>            filter-list-all = {!!}
>> 
>>            filter-member : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(pred
>>            : A →
>>            𝔹)(l : 𝕃 A) →
>>                             list-member eq a (filter pred l) ≡ tt →
>>                             list-member eq a l ≡ tt ∧ pred a ≡ tt
>>            filter-member = {!!}
>> 
>> 
>>            zip-unzip : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂}(x : 𝕃 A)(y :
>>            𝕃 B) →
>>                         length x ≡ length y → unzip (zip x y) ≡ x , y
>>            zip-unzip = {!!}
>> 
>> 
>> 
>> 
>>        _______________________________________________
>>        Agda mailing list
>>        Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>        https://lists.chalmers.se/mailman/listinfo/agda
>> 
>> 
>> 
>>    --
>>    Andreas Abel  <><      Du bist der geliebte Mensch.
>> 
>>    Department of Computer Science and Engineering
>>    Chalmers and Gothenburg University, Sweden
>> 
>>    andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>>    http://www2.tcs.ifi.lmu.de/~abel/
>>    _______________________________________________
>>    Agda mailing list
>>    Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>    https://lists.chalmers.se/mailman/listinfo/agda
>> 
>> 
> 
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
> 
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda