Changeset 2422 for src/joint/blocks.ma


Ignore:
Timestamp:
Oct 30, 2012, 4:23:09 PM (8 years ago)
Author:
tranquil
Message:

adapted joint to cl_call f

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r2286 r2422  
    239239definition seq_block_step_in_code ≝
    240240  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
    241   src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst.
     241  ∃hd,tl.l = hd @ [tl] ∧
     242  src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst.
    242243
    243244definition seq_block_fin_step_in_code ≝
    244245  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
    245   src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B).
     246  ∃hd,tl.l = hd @ [tl] ∧
     247  src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
    246248
    247249(* generates ambiguity even if it shouldn't
Note: See TracChangeset for help on using the changeset viewer.