<br><div class="gmail_quote">On Sat, Oct 2, 2010 at 2:01 AM, David Leduc <span dir="ltr"><<a href="mailto:david.leduc6@googlemail.com">david.leduc6@googlemail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
I insist. I am stuck with my goal that includes vertical bars. If only<br>
I knew the semantics of vertical bars in a goal...</blockquote><div><br></div><div>The vertical bar indicates that the function is stuck on a "with" argument. For instance,</div><div>if you have</div><div><br></div>
<div>foo x with bar x</div><div>... | c y = stuff</div><div><br></div><div>you might end up with a goal containing foo t | bar t, meaning that foo is stuck on the</div><div>value of bar t. The proper course of action in this case is to do the same "with". Here's</div>
<div>how the interaction would go:</div><div><br></div><div>proof : (x : A) -> P (foo x)</div><div>proof x = {! goal = P (foo | bar x) !}</div><div><br></div><div>--</div><div><br></div><div>proof x with bar x</div><div>
... | z = {! goal = P (foo | z) !}</div><div><br></div><div>--</div><div><br></div><div>proof x with bar x</div><div>... | c y = {! goal = P stuff !}</div><div><br></div><div>/ Ulf</div></div>