<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>It is not true. When you consider the case where y = true, we
      have that f true false = 1 by the definition f true x = 1. f y
      false = 2 does not hold definitionally because f true x = 1 has
      precedence.</p>
    <p>To avoid this kind of definition, you can use the --exact-split
      option. See
<a class="moz-txt-link-freetext" href="http://agda.readthedocs.io/en/latest/language/function-definitions.html#case-trees">http://agda.readthedocs.io/en/latest/language/function-definitions.html#case-trees</a>
      .<br>
    </p>
    <p>James<code class="samp docutils literal"><span class="pre"><br>
        </span></code></p>
    <div class="moz-cite-prefix">On 03/07/17 14:35, Manuel Bärenz wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:d31e3d21-4a48-e88c-d197-918ce74b7b47@enigmage.de">
      <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
      <p>I didn't try, but how about pattern match on y, for example in
        a with-clause? Then the proof should be refl.<br>
      </p>
      <br>
      <div class="moz-cite-prefix">On 2017-07-03 15:34, v0id_NULL wrote:<br>
      </div>
      <blockquote type="cite"
cite="mid:CAE3YR0Xf2M1hV8St1BcjyswNQrUSckfCnzd1cDu3sNbW26E5xQ@mail.gmail.com">
        <div dir="ltr">
          <div style="font-size:12.8px">Dear list,</div>
          <div style="font-size:12.8px"><br>
          </div>
          <div style="font-size:12.8px">Help me please. How can I prove
            type of p2?</div>
          <div style="font-size:12.8px"><br>
          </div>
          <div>
            <div><span style="font-size:12.8px">module M1 where</span></div>
            <div><span style="font-size:12.8px"><br>
              </span></div>
            <div>
              <div><span style="font-size:12.8px">open import Data.Nat
                  using (ℕ)</span></div>
              <div><span style="font-size:12.8px">open import Data.Bool
                  using (Bool; true; false)</span></div>
              <div><span style="font-size:12.8px">open import
                  Relation.Binary.PropositionalEquality using (_≡_;
                  refl)</span></div>
              <div><span style="font-size:12.8px"><br>
                </span></div>
              <div><span style="font-size:12.8px">f : Bool → Bool → ℕ</span></div>
              <div><span style="font-size:12.8px">f true x = 1</span></div>
              <div><span style="font-size:12.8px">f y false = 2</span></div>
              <div><span style="font-size:12.8px">f false true = 3</span></div>
              <div><span style="font-size:12.8px"><br>
                </span></div>
              <div><span style="font-size:12.8px">p1 : {x : Bool} → f
                  true x ≡ 1</span></div>
              <div><span style="font-size:12.8px">p1 = refl</span></div>
              <div><span style="font-size:12.8px"><br>
                </span></div>
              <div><span style="font-size:12.8px">p2 : {y : Bool} → f y
                  false ≡ 2</span></div>
              <div><span style="font-size:12.8px">p2 = {!!}</span></div>
              <div><span style="font-size:12.8px"><br>
                </span></div>
              <div><span style="font-size:12.8px">p3 : f false true ≡ 3</span></div>
              <div><span style="font-size:12.8px">p3 = refl</span></div>
            </div>
          </div>
          <div><br>
          </div>
        </div>
        <br>
        <fieldset class="mimeAttachmentHeader"></fieldset>
        <br>
        <pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se" moz-do-not-send="true">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
      </blockquote>
      <br>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>