# /home/laney/.irssi/irclogs/Freenode/#agda.log-20151127

acertain acertain --- Day changed Thu Nov 26 2015 (id _ _ id) with id defined without implicits causes an error, but id _ _ (id _ _) works, whats going on here? 26/11 03:38 nevermind i figured it out 26/11 03:54 I have a question... 26/11 08:54 is it possible to do induction on vectors in agda? 26/11 08:55 yes 26/11 09:02 i mean, the preferred way would be to just do a pattern matching definition 26/11 09:02 ok, using pattern matching is easy 26/11 09:05 ...and without pattern matching? 26/11 09:05 you can define an induction combinator by pattern matching 26/11 09:05 I was trying in a way similar to the induction combinator for natural numbers or lists 26/11 09:09 but without success... sigh 26/11 09:10 Could you have a look to my implementation? 26/11 09:13 yup, put it on lpaste.net or similar 26/11 09:14 vectors.agda :: https://gist.github.com/anonymous/10040e221a6fd01f7821 26/11 09:17 `forgetlength´ is a function based on vectrec: for every vector it returns the corresponding list. it works 26/11 09:19 oh, your type for vectrec is not general enough 26/11 09:20 ah 26/11 09:20 :) 26/11 09:20 vectrec : {A : Set} {P : forall {n} -> Set} → {n : ℕ} → Vect A n → P {zero} → ({m : ℕ} → A → Vect A m → P {m} xs → P {succ m}) → P {n} 26/11 09:22 P {m} xs ? 26/11 09:26 sorry, without xs 26/11 09:27 i thought you wanted the full dependent eliminator at first, but your listrec is not so i tried to delete the extra stuff :) 26/11 09:28 I'm a newbie in Agda. I'm using it to implement some natural deduction rules obtained in MLTT 26/11 09:32 {A : Set} (P : ∀ {n} → Vec A n → Set) → P vectnil → (∀ {n} x → P {n} xs → P (vectcons x xs)) → ∀ {n} → xs → P {n} xs -- dependent eliminator type 26/11 09:35 vectrec : {A : Set} (P : ∀ {n} → Vect A n → Set) → P vectnil → (∀ {n} x xs → P {n} xs → P (vectcons x xs)) → ∀ {n} xs → P {n} xs ? 26/11 09:52 vectnil has a different type 26/11 09:54 no, ok, I'm sorry... the order of the arguments 26/11 09:56 ah, yeah, i have the vector last, you can change that 26/11 09:57 ok 26/11 09:58 It does not work with vectmap 26/11 10:01 sigh 26/11 10:01 :) 26/11 10:01 may I have a look to your code? 26/11 10:03 _gio: see the comment on your gist 26/11 10:12 ok 26/11 10:13 woh 26/11 10:15 :D 26/11 10:15 what's the difference between vectrec and vectind ? 26/11 10:20 in vectind you are doing induction on ℕ and Vect ? 26/11 10:22 yeah, you can use it to prove things about vectors rather than just defining functions by recursion on them 26/11 10:23

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!