--- Day changed Sun Jan 07 2018
Nik05how can i change the tab width in agda mode? I am not a big emacs user, so no idea where i could find this option07/01 12:19
rntzby "tab width", what do you mean? do you mean, how many spaces a tab character displays as?07/01 13:40
rntzor do you mean something about what pressing the Tab key does?07/01 13:40
rntzto change how many spaces a tab character displays as, set the variable tab-width07/01 13:41
rntze.g. "M-: (setq tab-width 4)" or "M-x customize-variable RET tab-width"07/01 13:41
Nik05thank you rntz. I mean how to set how many space are set when pressing TAB07/01 13:45
rntzNik05: hm. can you do "C-h c TAB" in an agda-mode window and tell me what it says?07/01 13:47
rntzfor me it says "TAB (translated from <tab>) runs the command eri-indent"07/01 13:47
rntzit looks like eri-indent tries to indent to a position that aligns with something in the line above it07/01 13:49
rntzand otherwise indents by 2? which appears to be hardcoded? I'm just skimming eri-indent.el here.07/01 13:49
rntzso, if that's true, I'm not sure there is an easy way to customize indentation behavior in agda-mode :/07/01 13:49
Nik05oke let me check07/01 13:49
Nik05mine runs eri-indent as well07/01 13:50
Nik05oke thank you for finding out :)07/01 13:51
rntznp :)07/01 13:51
Nik05I got another question, about lambda that are function arguments07/01 13:51
rntzin emacs lisp or in agda?07/01 13:52
Nik05in agda07/01 13:52
rntzok, what's the question?07/01 13:52
Nik05when using refinement or automatic proof finding, it doesnt place braces around lambda's. Is this some problem in my precedence setup or is this default behaviour?07/01 13:52
rntzhm, that's odd. for me it does put parentheses around them.07/01 13:54
rntzwhat version of agda mode are you using?07/01 13:54
Nik052.5.307/01 13:54
rntzah, I'm using 2.5.207/01 13:55
rntzI don't know why it would have changed. hopefully someone else here will know?07/01 13:56
Nik05Oke, sometimes it does put braces around it07/01 13:57
Nik05really strange07/01 13:58
Nik05When I got something like this "foo { }0 { }1" and I refine on the first hole it looks like07/01 14:05
Nik05"foo λ x → {!!} {!!}" 07/01 14:06
Nik05if fill the first hole correctly, and do a reload of the file, I am getting errors07/01 14:07
trikl[m]Yeah, that lambda should go inside a parenthesis, the bodies of lambdas extend to the right in Agda07/01 14:09
Nik05is this a problem in the latest agda mode07/01 14:10
Nik05?07/01 14:10
Nik05trikl[m] it looks like I got a proof that doesn't really have lambdas in braces07/01 14:53
Nik05no idea what it does07/01 14:53
Nik05*how it does it without braces07/01 14:54
trikl[m]Nik05: Without parenthesis or braces the lambda stretch to the right07/01 15:14
trikl[m]lambdas*07/01 15:14
Nik05oh oke then it isnt needed07/01 15:14
trikl[m]No, not always07/01 15:15
Nik05is there any way to find the precedence of \to, lambdas etc?07/01 15:15
trikl[m]You can use parenthesis to delimit them, or alternatively braces if you want to pattern match on the arguments07/01 15:15
trikl[m]Not that I know of07/01 15:15
trikl[m]`(\ x -> x)` or `\ {x -> x}`07/01 15:17
Nik05oke07/01 15:17
trikl[m]In the second case, you can pattern match on `x`07/01 15:17
Nik05i read that the second case is not equal to the first07/01 15:17
trikl[m]Is there a difference in meaning?07/01 15:18
Nik05Something like (\x -> x) = (\x -> x), \{x -> x} != \{x -> x}07/01 15:18
trikl[m]I don't get what you mean07/01 15:20
Nik05"Currently, there is a semantic difference between regular and extended lambdas (i.e. without and with curly braces): regular lambdas are compared structurally, but each extended lambda introduces a new (anonymous) top-level function." -jespercockx on Github07/01 15:21
pgiarrussoNik05: looks like your guess is right07/01 16:16
pgiarrussoif you define f x = x; g x = x, f and g are not equal (neither definitionally nor propositionally, if you already know what that means)07/01 16:17
pgiarrussoyou can prove they’re propositionally equal if you postulate functional extensionality (which you can do, it is a sound axiom, but it’s sometimes annoying)07/01 16:18
pgiarrussothe comment you quote (which I didn’t know about) says that `\{x -> x}` translates to (1) take a fresh function name, let’s say `f`; (2) introduce a new top-level function `f x = x` (3) replace `\{x -> x}` with the name of the new to-level function, that is `f`07/01 16:19
pgiarrussohence two occurrences of `\{x -> x}` translate to *distinct* function names07/01 16:19
pgiarrussonone of this happens with `\x -> x`07/01 16:20
Nik05pgiarrusso thank you07/01 16:22
pgiarrussoNik05 :-)07/01 16:24
Nik05oke i get it :)07/01 16:26
trikl[m]http://people.inf.elte.hu/divip/AgdaTutorial/Index.html07/01 18:41
trikl[m]Found this, nice introductory material07/01 18:41

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