Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/JMCoercions.ma

    r1335 r1599  
    11include "basics/jmeq.ma".
    22include "basics/types.ma".
    3 include "basics/list.ma".
     3include "basics/lists/list.ma".
    44
    55definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
Note: See TracChangeset for help on using the changeset viewer.