Changeset 1599 for src/utilities


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.

Location:
src/utilities
Files:
1 deleted
7 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Coqlib.ma

    r761 r1599  
    1919
    2020include "basics/types.ma".
    21 include "basics/list.ma".
     21include "basics/lists/list.ma".
    2222
    2323include "ASM/Util.ma".
  • src/utilities/adt/priority_set_adt.ma

    r1223 r1599  
    11include "basics/types.ma".
    2 include "basics/list.ma".
     2include "basics/lists/list.ma".
    33include "arithmetics/nat.ma".
    44include "common/Integers.ma".
  • src/utilities/adt/set_adt.ma

    r1463 r1599  
    11include "basics/types.ma".
    2 include "basics/list.ma".
     2include "basics/lists/list.ma".
    33include "arithmetics/nat.ma".
    44include "ASM/Util.ma".
  • src/utilities/adt/table_adt.ma

    r1296 r1599  
    11include "basics/types.ma".
    22include "basics/bool.ma".
    3 include "basics/list.ma".
     3include "basics/lists/list.ma".
    44
    55include "arithmetics/nat.ma".
  • src/utilities/binary/division.ma

    r1528 r1599  
    5050  ]
    5151| p0 m' ⇒
    52   match divide m' n with
    53   [ pair q r ⇒
     52  let 〈q,r〉 ≝ divide m' n in
    5453    match r with
    5554    [ pzero ⇒ 〈natp0 q,pzero〉
     
    6160      ]
    6261    ]
    63   ]
    6462| p1 m' ⇒
    65   match divide m' n with
    66   [ pair q r ⇒
     63  let 〈q,r〉 ≝ divide m' n in
    6764    match r with
    6865    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
     
    7471      ]
    7572    ]
    76   ]
    7773].
    7874
     
    326322    [ OZ ⇒ OZ
    327323    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
    328     | neg m ⇒ match divide n m with [ pair q r ⇒
    329                 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     324    | neg m ⇒ let 〈q,r〉 ≝ divide n m in
     325                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ]
    330326    ]
    331327  | neg n ⇒
    332328    match y with
    333329    [ OZ ⇒ OZ
    334     | pos m ⇒ match divide n m with [ pair q r ⇒
    335                 match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
     330    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
     331                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ]
    336332    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
    337333    ]
     
    345341    [ OZ ⇒ OZ
    346342    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
    347     | neg m ⇒ match divide n m with [ pair q r ⇒
    348                 match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
     343    | neg m ⇒ let 〈q,r〉 ≝ divide n m in
     344                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ]
    349345    ]
    350346  | neg n ⇒
    351347    match y with
    352348    [ OZ ⇒ OZ
    353     | pos m ⇒ match divide n m with [ pair q r ⇒
    354                 match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
     349    | pos m ⇒ let 〈q,r〉 ≝ divide n m in
     350                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ]
    355351    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
    356352    ]
  • src/utilities/extralib.ma

    r1593 r1599  
    1414
    1515include "basics/types.ma".
    16 include "basics/list.ma".
     16include "basics/lists/list.ma".
    1717include "basics/logic.ma".
    18 include "utilities/pair.ma".
    1918include "ASM/Util.ma".
    2019
  • src/utilities/lists.ma

    r1551 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22
    33let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
Note: See TracChangeset for help on using the changeset viewer.