[Agda] Constructors are injective -- standard proof?

[Andreas Abel]

On 05.06.2014 16:20, Jacques Carette wrote:
> 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?

Datatypes are not generic, so you have to prove it for each type.

> 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.

Agreed.  In the github version of the std-lib these are now public under

   Data.Nat.Properties.Simple

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/