Nik05 rntz --- Day changed Sun Jan 07 2018 how can i change the tab width in agda mode? I am not a big emacs user, so no idea where i could find this option 07/01 12:19 by "tab width", what do you mean? do you mean, how many spaces a tab character displays as? 07/01 13:40 or do you mean something about what pressing the Tab key does? 07/01 13:40 to change how many spaces a tab character displays as, set the variable tab-width 07/01 13:41 e.g. "M-: (setq tab-width 4)" or "M-x customize-variable RET tab-width" 07/01 13:41 thank you rntz. I mean how to set how many space are set when pressing TAB 07/01 13:45 Nik05: hm. can you do "C-h c TAB" in an agda-mode window and tell me what it says? 07/01 13:47 for me it says "TAB (translated from ) runs the command eri-indent" 07/01 13:47 it looks like eri-indent tries to indent to a position that aligns with something in the line above it 07/01 13:49 and otherwise indents by 2? which appears to be hardcoded? I'm just skimming eri-indent.el here. 07/01 13:49 so, if that's true, I'm not sure there is an easy way to customize indentation behavior in agda-mode :/ 07/01 13:49 oke let me check 07/01 13:49 mine runs eri-indent as well 07/01 13:50 oke thank you for finding out :) 07/01 13:51 np :) 07/01 13:51 I got another question, about lambda that are function arguments 07/01 13:51 in emacs lisp or in agda? 07/01 13:52 in agda 07/01 13:52 ok, what's the question? 07/01 13:52 when 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 hm, that's odd. for me it does put parentheses around them. 07/01 13:54 what version of agda mode are you using? 07/01 13:54 2.5.3 07/01 13:54 ah, I'm using 2.5.2 07/01 13:55 I don't know why it would have changed. hopefully someone else here will know? 07/01 13:56 Oke, sometimes it does put braces around it 07/01 13:57 really strange 07/01 13:58 When I got something like this "foo { }0 { }1" and I refine on the first hole it looks like 07/01 14:05 "foo λ x → {!!} {!!}" 07/01 14:06 if fill the first hole correctly, and do a reload of the file, I am getting errors 07/01 14:07 Yeah, that lambda should go inside a parenthesis, the bodies of lambdas extend to the right in Agda 07/01 14:09 is this a problem in the latest agda mode 07/01 14:10 ? 07/01 14:10 trikl[m] it looks like I got a proof that doesn't really have lambdas in braces 07/01 14:53 no idea what it does 07/01 14:53 *how it does it without braces 07/01 14:54 Nik05: Without parenthesis or braces the lambda stretch to the right 07/01 15:14 lambdas* 07/01 15:14 oh oke then it isnt needed 07/01 15:14 No, not always 07/01 15:15 is there any way to find the precedence of \to, lambdas etc? 07/01 15:15 You can use parenthesis to delimit them, or alternatively braces if you want to pattern match on the arguments 07/01 15:15 Not that I know of 07/01 15:15 (\ x -> x) or \ {x -> x} 07/01 15:17 oke 07/01 15:17 In the second case, you can pattern match on x 07/01 15:17 i read that the second case is not equal to the first 07/01 15:17 Is there a difference in meaning? 07/01 15:18 Something like (\x -> x) = (\x -> x), \{x -> x} != \{x -> x} 07/01 15:18 I don't get what you mean 07/01 15:20 "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 Github 07/01 15:21 Nik05: looks like your guess is right 07/01 16:16 if 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 you 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 the 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 hence two occurrences of \{x -> x} translate to *distinct* function names 07/01 16:19 none of this happens with \x -> x 07/01 16:20 pgiarrusso thank you 07/01 16:22 Nik05 :-) 07/01 16:24 oke i get it :) 07/01 16:26 http://people.inf.elte.hu/divip/AgdaTutorial/Index.html 07/01 18:41 Found this, nice introductory material 07/01 18:41