[Agda] Re: vertical bars | in my goal

[Ulf Norell]

On Sat, Oct 2, 2010 at 2:01 AM, David Leduc <david.leduc6 at googlemail.com>wrote:

> I insist. I am stuck with my goal that includes vertical bars. If only
> I knew the semantics of vertical bars in a goal...


The vertical bar indicates that the function is stuck on a "with" argument.
For instance,
if you have

foo x with bar x
... | c y = stuff

you might end up with a goal containing foo t | bar t, meaning that foo is
stuck on the
value of bar t. The proper course of action in this case is to do the same
"with". Here's
how the interaction would go:

proof : (x : A) -> P (foo x)
proof x = {! goal = P (foo | bar x) !}

--

proof x with bar x
... | z = {! goal = P (foo | z) !}

--

proof x with bar x
... | c y = {! goal = P stuff !}

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101002/105704e1/attachment.html