--- Day changed Thu Mar 09 2017
subttleHi, would anyone be so kind as to please tell me what the type signature for a function which takes a (Vec A n) where the A is the carrier for a DecTotalOrder implementation should look like?09/03 03:36
subttlesig : ∀ {d₁ d₂ d₃} {D : DecTotalOrder d₁ d₂ d₃} {n : ℕ} → Vec {!   !} n09/03 03:40
subttlenot sure how to finish that, or if I'm even on the right track09/03 03:40
subttleIn Haskell I'd just make it a constraint or whatever, but I do not yet have the intuition for how to accomplish this in Agda :/09/03 03:40
gallaissubttle: http://agda.github.io/agda-stdlib/Relation.Binary.html#922409/03 03:49
gallaisA DecTotalOrder has a field containing its Carrier09/03 03:49
gallais`DecTotalOrder.Carrier D` should give you what you are looking for09/03 03:49
subttlegallais: excellent, I will give that a try!09/03 03:50
subttlethanks09/03 03:50
gallaisnp09/03 03:50
hrumphhi09/03 03:57
hrumphhow much thought has been put into making a proof assistant that's just a haskell library or bunch of haskell libraries, so you do your proving in haskell?09/03 03:58
christiansenhrumph: I know of two: HaskHOL and Ivor09/03 04:15
christiansenhrumph: https://ecaustin.github.io/haskhol/ and https://pdfs.semanticscholar.org/0149/b9756f7605647e0bef6af019a9dee73d3053.pdf09/03 04:16
quchenWhat does ∀ do exactly? It »feels« like it adds an (x : _) for all occurring variables after it. So far, so good.09/03 07:31
quchenBut when I go beyond » ∀ a. ----> { a : _ }« things become less clear to me.09/03 07:31
quchenFor example, ∀ a → (b : Set) → c09/03 07:32
quchenDoes this add a clause for c somehow?09/03 07:32
quchenWhat about  ∀ a (b : Set) c → d09/03 07:33
quchenDoes a prefixed »forall« simply mean »add gaps for all un-typed variables in the signature«?09/03 07:34
quchens/un-typed/not-explicitly-typed/09/03 07:34
--- Log closed Thu Mar 09 09:24:54 2017
--- Log opened Thu Mar 09 09:25:03 2017
-!- Irssi: #agda: Total of 124 nicks [0 ops, 0 halfops, 0 voices, 124 normal]09/03 09:25
-!- Irssi: Join to #agda was synced in 126 secs09/03 09:27
akr[m]byorgey: yeah you are of course right about even ∘ tail vs. odd ∘ tail09/03 10:25
akr[m]byorgey: thanks for the suggestion about bisimulation, unfortunately I'm not there yet :)09/03 10:25
akr[m]gallais: I have no idea what is going on in that code09/03 10:26
akr[m]especially things like, 'Stream.head (map f xs) = …'09/03 10:26
akr[m]I suppose that must be some fancy copattern notation09/03 10:32
akr[m]huh okay https://gist.github.com/puffnfresh/896057409/03 10:33
akr[m]that seems pretty cool09/03 10:34
gallaisakr[m]: yes, that's copatterns. You can also write in postfix position like so if you prefer: `map f xs .Stream.head = (...)`09/03 11:43
gallais(You may need parentheses? I don't know, I don't use postfix projections)09/03 11:43
quchenWhat’s the difference between »data X (n : A) : Set where« and »data X : A → Set where«?09/03 11:44
gallaisin the first one A is a parameter (it will be the same everywhere in the return type of the constructors)09/03 11:44
gallaisin the second one it's and index (it can vary between constructors)09/03 11:44
gallaise.g. in `Vec A n`, `A` is a parameter but `n` is an index09/03 11:45
quchengallais: Ah, and that’s why we rarely see »Vec n A«?09/03 11:47
gallaisYep.09/03 12:05
quchengallais: Alright, thanks!09/03 12:09
jacobianoh sexy, copatterns09/03 23:27
gallais:)09/03 23:30

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