Changeset 1599 for src/common


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.

Location:
src/common
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/common/AssocList.ma

    r789 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22
    33definition assoc_list ≝ λA, B. list (A × B).
  • src/common/Errors.ma

    r1598 r1599  
    1616include "basics/types.ma".
    1717include "basics/logic.ma".
    18 include "basics/list.ma".
     18include "basics/lists/list.ma".
    1919include "common/PreIdentifiers.ma".
    2020include "utilities/lists.ma".
  • src/common/Events.ma

    r1516 r1599  
    2222(*include "Floats.ma".*)
    2323include "common/Values.ma".
    24 include "basics/list.ma".
     24include "basics/lists/list.ma".
    2525include "utilities/extralib.ma".
    2626include "common/CostLabel.ma".
     
    161161  match T' with
    162162  [ Econsinf' t T'' NOTEMPTY ⇒
    163       match split_traceinf' t T'' NOTEMPTY with [ pair e tl ⇒
    164       Econsinf e (traceinf_of_traceinf' tl) ]
     163      let 〈e,tl〉 ≝ split_traceinf' t T'' NOTEMPTY in
     164      Econsinf e (traceinf_of_traceinf' tl)
    165165  ].
    166166
  • src/common/Floats.ma

    r961 r1599  
    5959
    6060axiom Fcmp_ne_eq:
    61   ∀ f1,f2. Fcmp Cne f1 f2 = ¬(Fcmp Ceq f1 f2).
     61  ∀ f1,f2. Fcmp Cne f1 f2 = (¬(Fcmp Ceq f1 f2)).
    6262axiom Fcmp_le_lt_eq:
    6363  ∀ f1,f2. Fcmp Cle f1 f2 = (Fcmp Clt f1 f2 ∨ Fcmp Ceq f1 f2).
  • src/common/Globalenvs.ma

    r1583 r1599  
    495495      let init ≝ extract_init init_info in
    496496      let 〈g,st〉 ≝ g_st in
    497         match alloc_init_data st init r with [ pair st' b ⇒
     497        let 〈st',b〉 ≝ alloc_init_data st init r in
    498498          let g' ≝ add_symbol ? id b g in
    499499            〈g', st'〉
    500         ] )
     500        )
    501501    init_env vars.
    502502
  • src/common/IOMonad.ma

    r797 r1599  
    1919match v with
    2020[ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
    21 | Value v' ⇒ match v' with [ pair v1 v2 ⇒ f v1 v2 ]
     21| Value v' ⇒ let 〈v1,v2〉 ≝ v' in f v1 v2
    2222| Wrong m ⇒ Wrong ?? T' m
    2323].
  • src/common/Mem.ma

    r1545 r1599  
    2828(*include "binary/Z.ma".*)
    2929(*include "datatypes/sums.ma".*)
    30 (*include "datatypes/list.ma".*)
     30(*include "datatypes/lists/list.ma".*)
    3131(*include "Plogic/equality.ma".*)
    3232
  • src/common/SmallstepExec.ma

    r1233 r1599  
    4747match s with
    4848[ Wrong m ⇒ e_wrong ??? m
    49 | Value v ⇒ match v with [ pair t s' ⇒
     49| Value v ⇒ let 〈t,s'〉 ≝ v in
    5050    match is_final ?? exec g s' with
    5151    [ Some r ⇒ e_stop ??? t r s'
    52     | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     52    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
    5353| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    5454].
     
    6565match s with
    6666[ Wrong m ⇒ e_wrong ??? m
    67 | Value v ⇒ match v with [ pair t s' ⇒
     67| Value v ⇒ let 〈t,s'〉 ≝ v in
    6868    match is_final ?? exec g s' with
    6969    [ Some r ⇒ e_stop ??? t r s'
    70     | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] ]
     70    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
    7171| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
    7272].
Note: See TracChangeset for help on using the changeset viewer.