[Agda] `let postulate ... in'

[Andreas Abel]

One work-around, though not the safest, would be to have a global

   postulate anything : forall {a}{A : Set a} -> A

and then write

   let fx=fy : f x =' f y
       fx=fy = anything
   in  here fx=fy

Cheers,
Andreas

On 16.08.13 11:18 AM, Sergei Meshveliani wrote:
> Please, what may be a work around for  ``let postulate ...'' in
>
>    case P? y of \
>    { (yes _) →  let postulate fx=fy : f x =' f y
>                 in  here fx=fy
>    ; ...
>    }
>    where
>    ...
> ?
>
> Agda-2.3.2.1 does not type-check  `let postulate'.
> It does accept  ...
>                  where
>                  postulate ...,
>
> but `where' is not allowed in this place of  ` -> ...'  of `case'.
>
> (Most often I set `postulate' as temporary, for debugging. Debugging
> becomes easier, and further I replace `postulate' with implementation).
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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