On Thu, 2015-11-26 at 16:07 +0300, effectfully wrote:
> Also, could someone say why it's not possible to `postulate' in a
> let-declaration?
>
postulate foo : Foo
does not work under `let'. Instead it works
foo : Foo
foo = anything
where anything is declared globally as
postulate anything : ∀ {a} {A : Set a} → A
Regards,
------
Sergei