Changeset 2666 for src/joint


Ignore:
Timestamp:
Feb 14, 2013, 11:49:48 AM (7 years ago)
Author:
piccolo
Message:

bug fixed in blocks.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r2599 r2666  
    381381  λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
    382382  ∃hd,tl.l = hd @ [tl] ∧
    383   src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
     383  src ~❨\fst B, hd❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
    384384
    385385interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
Note: See TracChangeset for help on using the changeset viewer.