Changeset 1599 for src/Clight/casts.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/casts.ma

    r1516 r1599  
    7676
    7777lemma split_left : ∀A,m,n,h,t.
    78   split A (S m) n (h:::t) = let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉.
     78  split A (S m) n (h:::t) = (let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉).
    7979#A #m #n #h #t normalize >split_eq' @refl
    8080qed.
Note: See TracChangeset for help on using the changeset viewer.