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/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.