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

--- Day changed Thu Nov 26 2015
acertain(id _ _ id) with id defined without implicits causes an error, but id _ _ (id _ _) works, whats going on here?26/11 03:38
acertainnevermind i figured it out26/11 03:54
_gioI have a question...26/11 08:54
_giois it possible to do induction on vectors in agda?26/11 08:55
Saizanyes26/11 09:02
Saizani mean, the preferred way would be to just do a pattern matching definition26/11 09:02
_giook, using pattern matching is easy26/11 09:05
_gio...and without pattern matching?26/11 09:05
Saizanyou can define an induction combinator by pattern matching26/11 09:05
_gioI was trying in a way similar to the induction combinator for natural numbers or lists26/11 09:09
_giobut without success... sigh26/11 09:10
_gioCould you have a look to my implementation?26/11 09:13
Saizanyup, put it on lpaste.net or similar26/11 09:14
_giovectors.agda :: https://gist.github.com/anonymous/10040e221a6fd01f782126/11 09:17
_gio`forgetlength´ is a function based on vectrec: for every vector it returns the corresponding list. it works26/11 09:19
Saizanoh, your type for vectrec is not general enough26/11 09:20
_gioah26/11 09:20
_gio:)26/11 09:20
Saizanvectrec : {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
_gioP {m} xs ?26/11 09:26
Saizansorry, without xs26/11 09:27
Saizani 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
_gioI'm a newbie in Agda. I'm using it to implement some natural deduction rules obtained in MLTT26/11 09:32
Saizan{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 type26/11 09:35
_giovectrec : {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
_giovectnil has a different type26/11 09:54
_giono, ok, I'm sorry... the order of the arguments26/11 09:56
Saizanah, yeah, i have the vector last, you can change that26/11 09:57
_giook26/11 09:58
_gioIt does not work with vectmap26/11 10:01
_giosigh26/11 10:01
_gio:)26/11 10:01
_giomay I have a look to your code?26/11 10:03
Saizan_gio: see the comment on your gist26/11 10:12
_giook26/11 10:13
_giowoh26/11 10:15
_gio:D26/11 10:15
_giowhat's the difference between vectrec and vectind ?26/11 10:20
_gioin vectind you are doing induction on ℕ and Vect ?26/11 10:22
Saizanyeah, you can use it to prove things about vectors rather than just defining functions by recursion on them26/11 10:23

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