[Agda] Do you use postulates extensively?

[Apostolis Xekoukoulotakis]

Since now, I have spent days proving trivial mathematical propositions
without knowing if the general theory/idea is correct.

This, of course, means that the theory is developed while programming in
Agda. It is not developed before using Agda.

I am thinking of using postulates extensively and prove things on paper
instead of doing it in Agda.
It is less safe but much faster. Then check the validity of the main Idea
with the use of the postulates. Only then try to prove some of the
postulates that might be a bit tricky.

At least for me, proofs that do not take part in the computation of a
program can remain postulates.

What is your strategy? Do you use postulates extensively? In my opinion
this is important enough that it needs to be put in the documentation. I
have wasted too much time proving trivial propositions and we do not have
to do that.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190116/c84fc881/attachment.html>