[Agda] Constructors are injective -- standard proof?

Jacques Carette carette at mcmaster.ca
Thu Jun 5 16:20:28 CEST 2014


General question:  Is there a proof in the standard library that 
constructors for inductive types are injective?  Or is this something 
that must be proven for every single data type?

Specific question: Is the proof that 'suc' is injective in the standard 
library?  I searched for it, and could not find it.  [Of course it is 
trivial, but it seems silly to rewrite this over and over again, which 
is what a 'standard' library is for].

Related specific question: Is there a reason why all those useful little 
lemmas are all private in Data.Nat.Properties?  I've had to reprove some 
of them because of that.  Which seems silly.

Jacques



More information about the Agda mailing list