--- Day changed Thu Mar 09 2017 | ||

subttle | Hi, 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 |
---|---|---|

subttle | sig : ∀ {d₁ d₂ d₃} {D : DecTotalOrder d₁ d₂ d₃} {n : ℕ} → Vec {! !} n | 09/03 03:40 |

subttle | not sure how to finish that, or if I'm even on the right track | 09/03 03:40 |

subttle | In 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 |

gallais | subttle: http://agda.github.io/agda-stdlib/Relation.Binary.html#9224 | 09/03 03:49 |

gallais | A DecTotalOrder has a field containing its Carrier | 09/03 03:49 |

gallais | `DecTotalOrder.Carrier D` should give you what you are looking for | 09/03 03:49 |

subttle | gallais: excellent, I will give that a try! | 09/03 03:50 |

subttle | thanks | 09/03 03:50 |

gallais | np | 09/03 03:50 |

hrumph | hi | 09/03 03:57 |

hrumph | how 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 |

christiansen | hrumph: I know of two: HaskHOL and Ivor | 09/03 04:15 |

christiansen | hrumph: https://ecaustin.github.io/haskhol/ and https://pdfs.semanticscholar.org/0149/b9756f7605647e0bef6af019a9dee73d3053.pdf | 09/03 04:16 |

quchen | What does ∀ do exactly? It »feels« like it adds an (x : _) for all occurring variables after it. So far, so good. | 09/03 07:31 |

quchen | But when I go beyond » ∀ a. ----> { a : _ }« things become less clear to me. | 09/03 07:31 |

quchen | For example, ∀ a → (b : Set) → c | 09/03 07:32 |

quchen | Does this add a clause for c somehow? | 09/03 07:32 |

quchen | What about ∀ a (b : Set) c → d | 09/03 07:33 |

quchen | Does a prefixed »forall« simply mean »add gaps for all un-typed variables in the signature«? | 09/03 07:34 |

quchen | s/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 secs | 09/03 09:27 | |

akr[m] | byorgey: yeah you are of course right about even ∘ tail vs. odd ∘ tail | 09/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 code | 09/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 notation | 09/03 10:32 |

akr[m] | huh okay https://gist.github.com/puffnfresh/8960574 | 09/03 10:33 |

akr[m] | that seems pretty cool | 09/03 10:34 |

gallais | akr[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 |

quchen | What’s the difference between »data X (n : A) : Set where« and »data X : A → Set where«? | 09/03 11:44 |

gallais | in the first one A is a parameter (it will be the same everywhere in the return type of the constructors) | 09/03 11:44 |

gallais | in the second one it's and index (it can vary between constructors) | 09/03 11:44 |

gallais | e.g. in `Vec A n`, `A` is a parameter but `n` is an index | 09/03 11:45 |

quchen | gallais: Ah, and that’s why we rarely see »Vec n A«? | 09/03 11:47 |

gallais | Yep. | 09/03 12:05 |

quchen | gallais: Alright, thanks! | 09/03 12:09 |

jacobian | oh sexy, copatterns | 09/03 23:27 |

gallais | :) | 09/03 23:30 |

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