<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Thu, Nov 20, 2014 at 5:33 AM, Gabriel Scherer <span dir="ltr">&lt;<a href="mailto:gabriel.scherer@gmail.com" target="_blank">gabriel.scherer@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I see that you end your post suggesting that Youtube may be a better<br>
distribution channel for your content. I beg to differ.</blockquote><div><br></div><div>Interesting. I actually have made a video, but I am not confident enough in my presentation skills to recommend it :). On the whole though, I tend to prefer videos. I think I&#39;ll try to use the blog posts as draft scripts for the videos.<br></div><div> <br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I like the post format, but if I was to point out a weak point, it is<br>
the use of screenshot. They take time for your to prepare, and they<br>
have lesser accessibility (for blind people for example) than text<br>
format (or even HTML). It would be nice to have a<br>
&quot;this-Agda-state-to-HTML&quot; command (that would also take into account<br>
the *Error* and other message buffers), or maybe even a way to<br>
interactively replay a proof (including errors) in a browser. The Coq<br>
community has developed a tool in that direction, Proviola :<br>
  <a href="http://mws.cs.ru.nl/proviola/" target="_blank">http://mws.cs.ru.nl/proviola/</a><br></blockquote><div><br></div><div>They&#39;re not actually so bad - Alt+PrtSc is all it takes, followed by an upload. I would *love* to use a tool like you&#39;re describing, but I&#39;m not really in a position to implement something like that myself right now. As for accessibility - well, I doubt I will reach a wide enough audience for that to matter xD<br><br></div><div>Thanks for the feedback. (I hope that this type of discussion isn&#39;t too off-topic for the mailing list...?)<br></div><div><br><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div><div class="h5"><br>
On Thu, Nov 20, 2014 at 12:52 AM, Christopher Jenkins<br>
&lt;<a href="mailto:cjenkin1@trinity.edu">cjenkin1@trinity.edu</a>&gt; wrote:<br>
&gt; All,<br>
&gt;<br>
&gt; The blog post I promised:<br>
&gt; <a href="http://serendependy.blogspot.com/2014/11/with-great-power-great-intractibility.html" target="_blank">http://serendependy.blogspot.com/2014/11/with-great-power-great-intractibility.html</a><br>
&gt;<br>
&gt; Feel free to add comments or suggestions on the blog itself or here.<br>
&gt;<br>
&gt; On Thu, Nov 6, 2014 at 3:39 PM, Andreas Abel &lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;<br>
&gt; wrote:<br>
&gt;&gt;<br>
&gt;&gt; Note that I am in the process of outlawing `with` on variables bound by<br>
&gt;&gt; module telescopes (because of the issue 1342 that came up during this<br>
&gt;&gt; discussion).<br>
&gt;&gt;<br>
&gt;&gt; Cheers,<br>
&gt;&gt; Andreas<br>
&gt;&gt;<br>
&gt;&gt; On 05.11.2014 23:53, Christopher Jenkins wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Alright, two people is enough to motivate me. I will try to have a first<br>
&gt;&gt;&gt; blog post out this weekend, mostly dealing with pattern-matching after a<br>
&gt;&gt;&gt; rewrite and the basic concept of `with&#39;, with more to follow.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; On Wed, Nov 5, 2014 at 2:21 AM, Arseniy Alekseyev<br>
&gt;&gt;&gt; &lt;<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a> &lt;mailto:<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;     Oh wow, I should have tried that. I don&#39;t understand why this works<br>
&gt;&gt;&gt; at<br>
&gt;&gt;&gt;     all. Note that none of these compile for me:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;        y | true   = id {A = (q : Bool) → x ≡ z q} (λ { true → refl ;<br>
&gt;&gt;&gt; false<br>
&gt;&gt;&gt;     → refl }) -- x != true of type Bool<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;        y | true   = id {A = (q : Bool) → true ≡ z q} (λ { true → refl ;<br>
&gt;&gt;&gt;     false → refl }) -- true != x of type Bool<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;     However, even more confusingly, this one does work:<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;        y | true   = id {A = _} (λ { true → refl ; false → refl })<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;     So what&#39;s the value of underscore it infers then?<br>
&gt;&gt;&gt;     Can anybody explain what&#39;s going on?<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;     As for the code smell part, I think you can only smell it on toy<br>
&gt;&gt;&gt;     examples, not on the &quot;real&quot; ones.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;     On 5 November 2014 01:28, Christopher Jenkins &lt;<a href="mailto:cjenkin1@trinity.edu">cjenkin1@trinity.edu</a><br>
&gt;&gt;&gt;     &lt;mailto:<a href="mailto:cjenkin1@trinity.edu">cjenkin1@trinity.edu</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt; On Tue, Nov 4, 2014 at 5:18 PM, Arseniy Alekseyev<br>
&gt;&gt;&gt;      &gt; &lt;<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a><br>
&gt;&gt;&gt;     &lt;mailto:<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;      &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; That was not a genuine attempt to prove `y : ∀ q → x ≡ z q`.<br>
&gt;&gt;&gt; Instead<br>
&gt;&gt;&gt;      &gt;&gt; that was an example of `with` rewriting the goal from (as you<br>
&gt;&gt;&gt;      &gt;&gt; demonstrated!) provable one into (as I assert) non-provable one.<br>
&gt;&gt;&gt; I<br>
&gt;&gt;&gt;      &gt;&gt; think that&#39;s the property of `with` that&#39;s causing you grief<br>
&gt;&gt;&gt;     when you<br>
&gt;&gt;&gt;      &gt;&gt; re-order or nest them in a bad way.<br>
&gt;&gt;&gt;      &gt;&gt;<br>
&gt;&gt;&gt;      &gt; Ah, makes sense. Though of course you could probably continue on<br>
&gt;&gt;&gt;     to prove<br>
&gt;&gt;&gt;      &gt; the goal by pattern-matching on a lambda argument introduced in<br>
&gt;&gt;&gt;     both cases,<br>
&gt;&gt;&gt;      &gt; but by that point hopefully someone would see the code smell.<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt; Actually, decided to include it anyway, so you could smell the<br>
&gt;&gt;&gt;     smelly code<br>
&gt;&gt;&gt;      &gt; smell:<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt;   y : ∀ q → x ≡ z q<br>
&gt;&gt;&gt;      &gt;   y with x<br>
&gt;&gt;&gt;      &gt;   y | true   = λ { true → refl ; false → refl }<br>
&gt;&gt;&gt;      &gt;   y | false  = λ { true → refl ; false → refl }<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; On 4 November 2014 22:43, Christopher Jenkins<br>
&gt;&gt;&gt;     &lt;<a href="mailto:cjenkin1@trinity.edu">cjenkin1@trinity.edu</a> &lt;mailto:<a href="mailto:cjenkin1@trinity.edu">cjenkin1@trinity.edu</a>&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; wrote:<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt; On Mon, Nov 3, 2014 at 2:38 PM, Arseniy Alekseyev<br>
&gt;&gt;&gt;      &gt;&gt; &gt; &lt;<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a><br>
&gt;&gt;&gt;     &lt;mailto:<a href="mailto:arseniy.alekseyev@gmail.com">arseniy.alekseyev@gmail.com</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; You are right, there is not much point. I was trying to point<br>
&gt;&gt;&gt;     out that<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; it&#39;s the &quot;proper expression&quot; part that makes `with`<br>
&gt;&gt;&gt; complicated.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; Unfortunately, that&#39;s not even true. In the following<br>
&gt;&gt;&gt;     example, I don&#39;t<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; think you can fill the holes.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; f : Bool → Bool<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; f x = true where<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;   z : Bool → Bool<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;   z true = x<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;   z false = x<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;   y : ∀ q → x ≡ z q<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;   y with x<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;   y | true = {!!}<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;   y | false = {!!}<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt; I&#39;m not entirely sure why you would expect that approach to be<br>
&gt;&gt;&gt;     fruitful.<br>
&gt;&gt;&gt;      &gt;&gt; &gt; Essentially, what you&#39;re trying to do is unwind the<br>
&gt;&gt;&gt;     computational nature<br>
&gt;&gt;&gt;      &gt;&gt; &gt; of<br>
&gt;&gt;&gt;      &gt;&gt; &gt; `z&#39;, which is defined by case analysis on its argument (in<br>
&gt;&gt;&gt;     this case q).<br>
&gt;&gt;&gt;      &gt;&gt; &gt; To<br>
&gt;&gt;&gt;      &gt;&gt; &gt; trigger the rules, you would have to bring q into scope and<br>
&gt;&gt;&gt;     inspect q,<br>
&gt;&gt;&gt;      &gt;&gt; &gt; which<br>
&gt;&gt;&gt;      &gt;&gt; &gt; would then lead to `z true&#39; and `z false&#39; in the equations,<br>
&gt;&gt;&gt;      &gt;&gt; &gt; respectively,<br>
&gt;&gt;&gt;      &gt;&gt; &gt; and Agda will then go on to normalize the goals as `x \== x&#39;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt; f : Bool → Bool<br>
&gt;&gt;&gt;      &gt;&gt; &gt; f x = true where<br>
&gt;&gt;&gt;      &gt;&gt; &gt;   z : Bool → Bool<br>
&gt;&gt;&gt;      &gt;&gt; &gt;   z true = x<br>
&gt;&gt;&gt;      &gt;&gt; &gt;   z false = x<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;   y : ∀ q → x ≡ z q<br>
&gt;&gt;&gt;      &gt;&gt; &gt;   y true = {!!} -- Goal: x ≡ x<br>
&gt;&gt;&gt;      &gt;&gt; &gt;   y false = {!!} -- Goal: x ≡ x<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt; I have actually been thinking about writing a blog post<br>
&gt;&gt;&gt;     targeted at<br>
&gt;&gt;&gt;      &gt;&gt; &gt; newbies<br>
&gt;&gt;&gt;      &gt;&gt; &gt; (such as myself) on the sometimes unintuitive behaviour of<br>
&gt;&gt;&gt;     `with&#39; (and<br>
&gt;&gt;&gt;      &gt;&gt; &gt; in<br>
&gt;&gt;&gt;      &gt;&gt; &gt; particular, `rewrite&#39;). Should anyone be interested I can send<br>
&gt;&gt;&gt;     a link on<br>
&gt;&gt;&gt;      &gt;&gt; &gt; this email chain once I have written it.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; On 3 November 2014 10:59, Andreas Abel<br>
&gt;&gt;&gt;     &lt;<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a> &lt;mailto:<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; On 03.11.2014 09:47, Arseniy Alekseyev wrote:<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; I think the problem goes away if you<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; only use `with x` where `x` is a variable.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; Mmh, why use `with` at all then?  You could directly split<br>
&gt;&gt;&gt;     on the<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; variable<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; `x`.  I thought the only reason to use `with` was when you<br>
&gt;&gt;&gt;     wanted to<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; case on<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; a proper expression and refine your type in the<br>
&gt;&gt;&gt;     with-branches...<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; On 03.11.2014 09:47, Arseniy Alekseyev wrote:<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; Indeed that&#39;s the usual Agda behaviour.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; Here the reason seems to be an additional occurrence of<br>
&gt;&gt;&gt;     `lookup k<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; ps`<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; in the context produced by pattern-match on `no`.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; You see, `with expr` only rewrites the occurrences of<br>
&gt;&gt;&gt;     `expr` present<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; in the enclosing context, so the new occurrences inside<br>
&gt;&gt;&gt;     the body of<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; `with` don&#39;t get rewritten (and you do want it rewritten<br>
&gt;&gt;&gt;     in this<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; case).<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; I do agree this is confusing. I think the problem goes<br>
&gt;&gt;&gt;     away if you<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; only use `with x` where `x` is a variable. That makes<br>
&gt;&gt;&gt;     `with` much<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; less<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; useful though. You can also avoid `with` altogether and<br>
&gt;&gt;&gt;     write the<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; helper functions by hand (that&#39;s what `with` is doing<br>
&gt;&gt;&gt;     after all!).<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; On 2 November 2014 17:14,  &lt;<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a><br>
&gt;&gt;&gt;     &lt;mailto:<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>&gt;&gt; wrote:<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; People,<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; Having the proof<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    prove : (k∈ks : k ∈ ks) → proj₂ (lookupIf∈ k (p ∷ ps)<br>
&gt;&gt;&gt;     k∈k&#39;:ks) ≡<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;                              proj₂ (lookupIf∈ k ps k∈ks)<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    prove k∈ks  with  k ≟ k&#39;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; --<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; (I)<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    ... | yes k≡k&#39; =  ⊥-elim $ k≉k&#39; k≡k&#39;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    ... | no _     with  lookup k ps<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    ...                | inj₁ _    =  PE.refl<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    ...                | inj₂ k∉ks =  ⊥-elim $ k∉ks k∈ks<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; (I do not give the complete code),<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; I try to rewrite it in a bit simpler way by joining it<br>
&gt;&gt;&gt;     into one<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; `with&#39;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; clause:<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    prove k∈ks  with  k ≟ k&#39; | lookup k ps<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; --<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; (II)<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    ... | yes k≡k&#39; | _         =  ⊥-elim $ k≉k&#39; k≡k&#39;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    ... | no _     | inj₁ _    =  PE.refl<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;    ... | no _     | inj₂ k∉ks =  ⊥-elim $ k∉ks k∈ks<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; (I) is type-checked, and (II) is not.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; Is this natural for Agda to decide so?<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; (I have spent 4 hours trying to prove a similar real and<br>
&gt;&gt;&gt;     evident<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; example.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; Then tried to split `with&#39; into two, and this has<br>
&gt;&gt;&gt; succeeded).<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; Thanks,<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; ------<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; Sergei<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; Agda mailing list<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; Agda mailing list<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; --<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; Department of Computer Science and Engineering<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; Chalmers and Gothenburg University, Sweden<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a> &lt;mailto:<a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a>&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; &gt; <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; _______________________________________________<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; Agda mailing list<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>&gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt;<br>
&gt;&gt;&gt;      &gt;&gt; &gt; --<br>
&gt;&gt;&gt;      &gt;&gt; &gt; Christopher Jenkins<br>
&gt;&gt;&gt;      &gt;&gt; &gt; Computer Science 2013<br>
&gt;&gt;&gt;      &gt;&gt; &gt; Trinity University<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt;<br>
&gt;&gt;&gt;      &gt; --<br>
&gt;&gt;&gt;      &gt; Christopher Jenkins<br>
&gt;&gt;&gt;      &gt; Computer Science 2013<br>
&gt;&gt;&gt;      &gt; Trinity University<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; --<br>
&gt;&gt;&gt; Christopher Jenkins<br>
&gt;&gt;&gt; Computer Science 2013<br>
&gt;&gt;&gt; Trinity University<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; --<br>
&gt;&gt; Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
&gt;&gt;<br>
&gt;&gt; Department of Computer Science and Engineering<br>
&gt;&gt; Chalmers and Gothenburg University, Sweden<br>
&gt;&gt;<br>
&gt;&gt; <a href="mailto:andreas.abel@gu.se">andreas.abel@gu.se</a><br>
&gt;&gt; <a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; --<br>
&gt; Christopher Jenkins<br>
&gt; Computer Science 2013<br>
&gt; Trinity University<br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
</div></div>&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
</blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div>Christopher Jenkins<br>Computer Science 2013<br>Trinity University</div></div></div>
</div></div>