The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 08/19/2016 07:47 PM, Jonathan Leivent wrote:
> Would you even recognize the decompiled lemma as the one you intended,
> based on all that would need to be omitted (notations, implicits,
> unicode translations, coercions, etc.)?
Depends on the lemma of course. If you ask it to print a lemma whose 
statement heavily relies on notations and implicit arguments, it will 
probably be unrecognizable.

However, that does not have to be the case. Take a look at:


https://github.com/math-comp/math-comp/blob/master/mathcomp/odd_order/stripped_odd_order_theorem.v

This is a rather small self-contained file that consists of the 
odd-order theorem and all definitions involved in its statement. It does 
not rely on notations, implicit arguments, and so on.