--- Day changed Wed Feb 08 2017
akrmietek: yeah it seems that pretty printing is broken for them as well08/02 08:13
akrthe stdlib is confusing; how do I open PreorderReasoning if what I have is a record of type IsEquivalence?08/02 09:17
{AS}akr: can you show your code08/02 09:18
{AS}usually you can do open PreorderReasoning (isPreorder equiv)08/02 09:19
akr{AS}: https://gist.github.com/osense/daf261d34184468d7024aba280cf338208/02 09:19
{AS}where equiv is IsEquivalence08/02 09:19
{AS}so you can do08/02 09:20
{AS}open PreorderReasoning (isPreorder M.isEq )08/02 09:20
{AS}akr: ^08/02 09:20
{AS}or you may have to use IsEquivalence.isPreorder08/02 09:22
akrIsEquivalence doesn't have a field like that though08/02 09:22
akrhttps://agda.github.io/agda-stdlib/Relation.Binary.Core.html#483308/02 09:23
{AS}akr: sorry08/02 09:23
{AS}you are right08/02 09:23
{AS}I looked the right place08/02 09:24
{AS}wrong*08/02 09:24
{AS}akr: you probably do need to make the preorder manually08/02 09:26
akrseems like it08/02 09:26
{AS}akr: or you could define your thing as a setoid08/02 09:27
{AS}and use preorder08/02 09:27
{AS}akr: basically08/02 09:27
{AS}you can define C-setoid : Setoid lzero lzero; C-setoid = record { Carrier = C;  _≈_ = _≈_; isEquivalence = isEq }08/02 09:29
{AS}akr: or you could just take C being a setoid08/02 09:29
{AS}and then use Carrier C instead of C in the rest of the operations08/02 09:30
{AS}or something like that08/02 09:30
akrI constructed it manually08/02 09:35
akrbut there's something wrong with instance resolution08/02 09:35
{AS}akr: what issue?08/02 09:35
akrit works on one line and then refuses on another08/02 09:35
akralthough possibly I'm just doing something wrong08/02 09:36
akryeah it's my fault; preorder needs two relations08/02 09:43
akrnever knew how hard is it to prove that an equivalence is a preorder -_-08/02 09:44
{AS}akr: that is why I said it was easier to construct the setoid instance08/02 09:46
{AS}and just use Setoid.preorder :)08/02 09:46
akrI'm not sure whether that is going to wirk with IsBooleanAlgebra08/02 09:52
akrwork*08/02 09:52
akrhmm but it should I think08/02 09:53
akr{AS}: got it to work, thanks for helping08/02 10:06
{AS}akr: np :)08/02 11:01
rntzis there a way to ask agda-mode to case-analyse a variable "as much as possible"?08/02 17:44
rntzsupposing myvar : A x (B x C), to turn it into (x , (x1 , x2))08/02 17:44
rntzinstead of just (x , x1)08/02 17:45
rntzunreatedly, is  there a way to change the fixity of something imported from another module? (say, to make _,_ right-associative)08/02 17:47
comietekrntz: do you see the variable in the goal display you get with C-c C-,?08/02 18:11
comietekrntz: if so, you could try C-u C-u C-c C-,08/02 18:12
akrIsn't the Boolean Algebra defined in stdlib missing axioms for identity elements?08/02 19:53
akrhttps://agda.github.io/agda-stdlib/Algebra.Structures.html#1325508/02 19:53
akrah no nevermind08/02 19:56
mietekakr: feel the pain of the stdlib08/02 20:38
mietekakr: FYI this is why my recent gists have been carrying an embedded mini-stdlib08/02 20:38
mietekakr: it actually includes equivalence-reasoning08/02 20:39
rntzcomietek: that just shows me its type, expanded more. I'm trying to get it to generate cases, like C-c C-c does.08/02 20:43
akrmietek: yeah the stdlib is… underwhelming08/02 20:46
akrI was checking out the prelude, but that seems mostly oriented on programming, not theorem proving08/02 20:46
akrthough I also wish there was more automation08/02 20:47
mietekrntz: have you tried the C-u C-u prefix in that situation?08/02 20:51
mietekI’m not clear what you wish to do08/02 20:52
mudrirntz: I understand what you're trying to do (and I have wished for the same), but I don't think there's anything for it in agda-mode.08/02 20:54
joebobjoedoes agda fully support using dependent types involving properties of floating point numbers?08/02 21:15
joebobjoeor is it too complex08/02 21:15
joebobjoeI know ATS gave up08/02 21:15
{AS}joebobjoe: I mean you could encode a theory of IEEE fp arithmetic08/02 21:21
{AS}I am unsure whether it is currently available08/02 21:21
{AS}You could also work with rationals08/02 21:21
mietekI think there were some improvements made recently to that08/02 21:31
mietekhttps://github.com/agda/agda/blob/master/CHANGELOG.md08/02 21:32
mietek"The built-in floats have new semantics to fix inconsistencies and to improve cross-platform portability. …"08/02 21:32
joebobjoehm08/02 21:53
glguyrntz: It may or may not be related to your question, but you can use macros in Agda to expand things by cases. I have an example in the last line of https://glguy.net/mockingbird-html/Dark-forest.html08/02 23:50
glguyI don't know of an agda-mode command to case split as much as possible, though08/02 23:51

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