[Agda] Re: where definitions and with

[Guillermo Calderon]

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
>
>