[Agda] `let postulate ... in'

Sergei Meshveliani mechvel at botik.ru
Fri Aug 16 11:18:32 CEST 2013

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

Agda- does not type-check  `let postulate'.
It does accept  ...
                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). 



More information about the Agda mailing list