[Agda] Re: where definitions and with

[Andreas Abel]

Ah, I see what you meant.

Unfortunately, where clauses apply only to a single clause at the 
moment, they cannot span over several clauses.  This would be a useful 
language extension, I guess, but not totally trivial.

Note that variable identity over several clauses is not entirely 
trivial.  While such obfuscation is not recommended, the following is 
entirely legal Agda:

   bla : Bool → Bool → Bool
   bla x y with blub
     where blub = not y
   bla a b | true = a
   bla y x | false = x

A work around for your problem might (or might not) be a pattern like:

   ff x y z = aux
     where
       foo = ... x y z ...
       aux : ...
       aux with foo
       ... | pat = ?

But if this works for you, you might as well use case.

Cheers,
Andreas

On 22.07.2015 16:32, Guillermo Calderon wrote:
>
> Andreas,
> Thanks for your answer.
>
> In fact, I meant:
>
>       ff  x y z  with foo
>       ... | pat = ?
>             where foo =  <something  depending on x y z>
>
> I should correct it as follows:
>
>
>       ff  x y z  with foo
>         where foo =  <something  depending on x y z>
>       ... | pat = ?
>
> But this way,  "foo" is not in the scope of the rhs.
> (Perhaps, I should use "case" instead of "with")
>
> Thanks again.
> Guillermo
>
> On 22/07/15 05:55, Andreas Abel wrote:
>> For me, this works:
>>
>>    test : Bool → Bool
>>    test x with y
>>      where y = not x
>>    test x | z = z
>>
>>    correct : ∀ b → test b ≡ not b
>>    correct true  = refl
>>    correct false = refl
>>
>> The code you wrote should give a parse error, as after a `with` there
>> cannot be an `= rhs`.
>>
>>     ff  x y z  with foo = ?
>>
>> Cheers,
>> Andreas
>>
>> On 21.07.2015 17:31, Guillermo Calderon wrote:
>>> People:
>>>
>>>
>>> Sometimes, I find convenient to write something like that:
>>>
>>>
>>>      ff  x y z  with foo = ?
>>>           where foo =  <something  depending on x y z>
>>>
>>>
>>> But Agda rejects it:  "not in scope foo ..."
>>>
>>> I conclude that the scope of where definitions does not include the
>>> "with" construct.
>>> Is there a good reason for this restriction?
>>>
>>>
>>>
>>> Thanks
>>> Guillermo
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/