<div dir="ltr"><div><div><div><div><div>With Andreas commit, the behavior is to replicate the style the programmer used, which means that nothing will change for you.<br><br></div>I do remember being confused by <br></div>"{x = x}" as well when I was learning the language.<br><br></div>I am too battling with cleaning the code so as to be readable. <br>A very important thing is to learn when to use implicit vs explicit arguments. <br>I haven't mastered that yet.<br><br></div>I also wonder whether there is a difference in complexity between mathematical proofs and software development.<br></div>As far as I know, Mathematics are characterized by elegance and simplicity.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 10, 2017 at 10:00 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thanks, Martin,<br>
<br>
for the explanation. I can confirm that a named argument like<br>
<br>
{x = x}<br>
<br>
can cause quite some confusion to the reader. (It looks non-sensical unless you are familiar with the specifics of Agda syntax.)<br>
<br>
Now, if you look at the bug report<br>
<br>
<a href="https://github.com/agda/agda/issues/2537" rel="noreferrer" target="_blank">https://github.com/agda/agda/i<wbr>ssues/2537</a><br>
<br>
you see that the current situation is incoherent. Agda preserves named arguments in the usual case, but not for with-clauses. I think that should be fixed.<br>
<br>
The next question is whether Agda should *introduce* named arguments or rather use a sequence of {_} arguments when, for instance, you split on a hidden argument.<br>
<br>
For your taste, Agda should not introduce named arguments ever in printing. Maybe a flag like<br>
<br>
--no-named-arguments<br>
<br>
could represent this style of printing terms.<br>
<br>
On 07.04.2017 16:23, Martin Escardo wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 07/04/17 15:01, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Martin,<br>
<br>
when it comes to interactive editing, we are striving for the commands<br>
to preserve/imitate the user code as much as possible. Thus, if the<br>
user has chosen named arguments, the splitter should preserve this<br>
style, instead of switching to positional arguments.<br>
<br>
Why are you fond of the current behavior?<br>
</blockquote>
<br>
Because, for personal idiosyncratic reasons, I don't use named<br>
arguments. Writing {x = x} {y = y} doesn't look idiomatic, and is<br>
confusing for people who don't know Agda but who I want to be able to<br>
understand my code. I write the Agda code for myself to read, and not<br>
for simply having something accepted and blessed by the Agda typchecker.<br>
If you are never going to write {x = a}, and you write always {x = x},<br>
this seems a wrong design. And {x = x} looks very curious and cryptic.<br>
Anyway, you can safely ignore my opinion. But this is what it is.<br>
Additionally I think adding variables that are not used in types makes<br>
the types very unreadable.<br>
<br>
Best,<br>
Martin<br>
<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Best,<br>
Andreas<br>
<br>
On 07.04.2017 16:02, Martin Escardo wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Andreas, for several reasons, I like the way things are regarding<br>
this. If there is any change, could it be achieved by a different<br>
control sequence, so as to preserve the existing behaviour? Thanks,<br>
Martin<br>
<br>
On 07/04/17 13:33, Andreas Abel wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Agda uses {_} to skip unsupplied hidden arguments. Instead it could use<br>
a named hidden argument for the supplied one {frll}.<br>
<br>
Could you put a reasonably small self-contained test case on the issue<br>
tracker?<br>
<br>
Thanks,<br>
Andreas<br>
<br>
On 07.04.2017 13:59, Apostolis Xekoukoulotakis wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
```<br>
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁)<br>
(_←⊂ {lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) |<br>
(drepl=>repl+ {frll = frll} ind lind)<br>
... | g | r = {!!}<br>
<br>
```<br>
case splitting creates this:<br>
<br>
```<br>
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁)<br>
(_←⊂ {lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) |<br>
(drepl=>repl+ {frll = frll} ind lind)<br>
removeCom {_} {_} {_} {_} {_} {frll} (_⊂_ {pll} {_} {_} {_} {ind} lf<br>
lf₁) (_←⊂ {_} {_} {_} {_} {_} {_} {_} {lind} ic) | .(replLL _ (ind +ᵢ<br>
lind) frll) | refl = ?<br>
```<br>
<br>
instead of :<br>
<br>
```<br>
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁)<br>
(_←⊂ {lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) |<br>
(drepl=>repl+ {frll = frll} ind lind)<br>
removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁)<br>
(_←⊂ {lind = lind} ic) | .(replLL _ (ind +ᵢ lind) frll) | refl = ?<br>
```<br>
<br>
I wonder if the behavior can be changed.<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>
</blockquote>
<br>
</blockquote>
<br>
<br>
</blockquote>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~ab<wbr>ela/</a><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>