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

--- Day changed Mon May 08 2017
subttleIf I want to use Data.AVL.Set with a type for which I have defined the StrictTotalOrder with my own equivalence relation, is that possible to do?08/05 10:37
subttleI'm using the line:08/05 10:37
subttleopen Data.AVL {Key = RegExp} {_<_ = _<r_} (StrictTotalOrder.isStrictTotalOrder sto)08/05 10:38
subttleand I get a type error:08/05 10:38
{AS}subttle: basically you just need to define the IsStrictTotalOrder08/05 10:38
subttleexpected x ≡ x, actual x ≡r x08/05 10:38
{AS}subttle: Ah, it seems that the implementation depends on the equality one08/05 10:39
{AS}subttle: so I would think not unless you redefine it08/05 10:40
subttle{AS}: Thank you for your reply. Do you mean redefine my `sto`? Or something else?08/05 10:40
{AS}subttle: no the library08/05 10:40
{AS}I think it's currently depending on strict equality08/05 10:41
subttle{AS}: hm, do you imagine there is a reason it's not parameterized?08/05 10:41
{AS}My guess it's harder to implement otherwise08/05 10:42
subttle{AS}: I see, thank you for your help!08/05 10:42
{AS}np08/05 10:43

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