[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