[Agda] where definitions and with

[Andreas Abel]

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


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