[Agda] Do you use postulates extensively?

Nils Anders Danielsson nad at cse.gu.se
Wed Jan 16 11:49:00 CET 2019


On 16/01/2019 00.56, Apostolis Xekoukoulotakis wrote:
> Do you use postulates extensively?

No, but I can imagine that this depends on what you are working on. If
your subject of study depends on a lot of prior, very solid work, then
it might make sense to use postulates.

When I prove something under an assumption that cannot be proven (say,
"assuming equality of functions is extensional…") I have found it useful
to state the assumption explicitly rather than using postulates. This
makes it easy to track exactly what parts of the development depend on
what assumptions.

-- 
/NAD


More information about the Agda mailing list