--- Day changed Fri Mar 03 2017
rntzdoes it cause any problems if one postulates extensionality in agda?03/03 11:17
akrthis is somewhat interesting: https://ekaschalk.github.io/post/prettify-mode/03/03 11:30
akrI'm not sure which approach is better: use unicode directly in your code, or use only ASCII and hava your editor print them as unicode03/03 11:31
TanebI use unicode mostly to use the standard library03/03 11:32
TanebAnd if I'm using the standard library anyway why not use more unicode03/03 11:32
TanebBut if I'm not using the standard library then I try to use it less03/03 11:32
akrbut unicode is pretty :P03/03 11:36
Tanebakr, I think Agda looks a lot more impressive when I'm showing my friends if it's not a series of white squares on their computers03/03 11:37
akrif they could see the unicode characters, it would look even more impressive, surely03/03 11:40
akrI'm using predicates to encode sets, and I have a 2-element set: {a, b} and I want to define a set of sets (predicate on sets) on this: {∅, {a}, {a,b}}03/03 13:15
akrcan I encode this as  λ A → b ∈ A → b ∈ A03/03 13:16
akrand is there a better way03/03 13:16
akror should I just stop03/03 13:16
francoisbabeufThat's the normal way03/03 13:16
francoisbabeufIt's actually in the standard library03/03 13:16
akrit's not very pleasent to work with, though, is it03/03 13:17
akrpleasant03/03 13:17
francoisbabeufNo :) I ended up writing my own03/03 13:18
francoisbabeufThere is also a finite sets lib which is a bit better, but still not quite what I was after. 03/03 13:18
francoisbabeufhttps://github.com/GavinMendelGleason/code/blob/master/agda/MuPositivity/Membership.agda03/03 13:19
akrI also played with encoding sets as decidable predicates, i.e. A → Bool03/03 13:21
akrthen you get some nice stuff like A ∪ A' is all03/03 13:21
akrbut it was worse somehow03/03 13:21
francoisbabeufS ⊆ T = ∀ x → x ∈ S → x ∈ T03/03 13:21
akrI mean on the type level, talking about these things03/03 13:21
akroh I actually have a type there, I meant   λ A → b ∈ A → a ∈ A03/03 13:22
akrtypo*03/03 13:22
francoisbabeufYeah, I figured03/03 13:22
akrit has become unreasonably difficult to prove that if b ∈ (large union) and b ∈ A → a ∈ A, then a ∈ (large union)03/03 13:26
akrI wonder if you could make something like equational reasoning is for ≡ to work on this03/03 13:28
akralso, I am not sure why given some decidable predicate P : A → Bool, 'with P a' allows Agda to simplify the goal based on whether P a is true or false, but 'if P a then … else …' doesn't03/03 13:32
akrI guess because with is a primitive and if_then_else is not03/03 13:40
mudriIs there an equivalent to the C-u prefix in Spacemacs/Evil?03/03 15:35
mudriI don't know whether C-u is a general Emacs thing, or a particularly agda-mode thing.03/03 15:36
glguymudri: For the first C-u in evil mode you press Space U03/03 16:15
glguyso: Space U C-U C-C C-,03/03 16:15
glguyfor example03/03 16:15
glguyYou'll feel like a real emacs user as you bring up information about the current goal with definitions expanded03/03 16:16
mudriglguy: thanks.03/03 17:16
XenasisI'm writing a paper with literate Agda, and I want to reuse some names when implementing the same thing differently, with a desired effect like: http://lpaste.net/2473943824406151168 03/03 19:49
XenasisWhen these were different files, it was fine, but I'm unsure if there's a good way to do this without putting 'private' on everything (I can't find a way to apply that to a whole module)03/03 19:50
Xenasisany ideas?03/03 19:50
serendependyXenasis: If they're in different modules they should have different namespaces, even if they're in the same file. Are you indenting your "data A" to be within modules one and two?03/03 20:12
XenasisI am not indenting it at all in either case03/03 20:15
serendependyXenasis: lpaste.net/35318803/03 20:16
serendependyThen that's probably why you're getting name conflicts :)03/03 20:16
Xenasishm, I see03/03 20:17
Xenasisthanks! Going to see if I can fix it with playing around03/03 20:18
XenasisI had previously had these in two seperate files, which of course isn't workable for a big .lagda file03/03 20:18
mudriI have a declaration of type ∀ {x x′ y y′} → x ≈ x′ → y ≈ y′ → x ≈ y → x′ ≈ y′. Does “kan” make sense as a name, or is kan composition something more specific?03/03 20:57
akr"Is there an equivalent to the C-u prefix in Spacemacs/Evil?" I'm not sure what exactly that prefix does in plain emacs, but isn't what you're looking for Space m?03/03 20:58
akri.e. the commands from the Agda mode03/03 20:58
mudriakr: glguy answered earlier. I was thinking of specifically C-u C-u, which makes things print normalised. SPC-u C-u does an okay job of this, but means falling back on Emacs bindings.03/03 21:03
akrah, I see03/03 21:05
mudriMaybe the fact that I remap leader-u changes things, though.03/03 21:05
mudri(SPC u, not SPC-u)03/03 21:05
akrSPC u does the same thing as SPC-u for me03/03 21:06
mudriHolding SPC?03/03 21:09
mudriOh, SPC u SPC u <leader> <cmd> also works.03/03 21:10
akrwhat do you have space mapped to?03/03 21:11
mudriSPC is Spacemacs' eponymous space.03/03 21:12
mudriI haven't changed that (I think).03/03 21:12
akrokay03/03 21:13
akrthen what is <leader>03/03 21:13
mudriThat's set by dotspacemacs-major-mode-leader-key, which for me is \.03/03 21:17
mudriSPC m should also work.03/03 21:17
akrhmm, interesting, I thought space was leader03/03 21:18
mudridotspacemacs-leader-key is indeed SPC, now I check. I guess I never learnt it properly, and referred to the leader as “space”.03/03 21:20
mudriOh gosh, there's dotspacemacs-leader-key, dotspacemacs-emacs-leader-key, dotspacemacs-major-mode-leader-key, and dotspacemacs-major-mode-emacs-leader-key. :-|03/03 21:21
akrhaha03/03 21:22
akrI think that's enough for me for today03/03 21:22
mudriAnyway, it turns out that kan is a useful combinator for equation-style high-school-style proofs (rather than expression-style proofs offered by PreorderReasoning):03/03 21:28
lpaste_mudri pasted “No title” at http://lpaste.net/35319203/03 21:28

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