Changeset 697 for src/utilities


Ignore:
Timestamp:
Mar 18, 2011, 1:28:33 PM (9 years ago)
Author:
campbell
Message:

Merge Clight branch of vectors and friends.
Start making stuff build.

Location:
src/utilities
Files:
4 edited
1 moved

Legend:

Unmodified
Added
Removed
  • src/utilities/Coqlib.ma

    r695 r697  
    1818    library. *)
    1919
    20 include "binary/Z.ma".
     20include "utilities/binary/Z.ma".
    2121include "basics/types.ma".
    2222include "basics/list.ma".
    2323
    24 include "extralib.ma".
     24include "utilities/extralib.ma".
    2525
    2626(*
  • src/utilities/binary/Z.ma

    r487 r697  
    1717
    1818(*include "arithmetics/compare.ma".*)
    19 include "binary/positive.ma".
     19include "utilities/binary/positive.ma".
    2020
    2121inductive Z : Type[0] ≝
  • src/utilities/binary/positive.ma

    r487 r697  
    1717include "basics/logic.ma".
    1818include "arithmetics/nat.ma".
    19 include "oldlib/eq.ma".
     19include "utilities/oldlib/eq.ma".
    2020
    2121(* arithmetics/comparison.ma --> *)
     
    365365
    366366theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m.
    367 /3/; qed.
     367#n #m @not_to_not @le_S_S_to_le qed.
    368368
    369369theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m.
    370 /3/; qed.
     370#n #m @not_to_not /2/ qed.
    371371
    372372theorem decidable_le: ∀n,m:Pos. decidable (n≤m).
  • src/utilities/extralib.ma

    r695 r697  
    1616include "basics/list.ma".
    1717include "basics/logic.ma".
    18 include "binary/Z.ma".
    19 include "binary/positive.ma".
     18include "utilities/binary/Z.ma".
     19include "utilities/binary/positive.ma".
    2020
    2121lemma eq_rect_Type0_r:
Note: See TracChangeset for help on using the changeset viewer.