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

adapted joint to cl_call f

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2324 r2422  
    232232  %* #H @H -H
    233233  lapply tl_other lapply rest_in_code
    234   (* BUG? cases tl causes "Ill formed pattern" *)
    235   @(match tl with [ nil ⇒ ? | cons hd' tl' ⇒ ?])
     234  cases tl [2: #hd' #tl' ]
    236235  cases rest [2,4: #mid' #rest']
    237   [1,4: * ]
     236  [2,3: * ]
    238237  [2: whd in ⊢ (%→?); #EQ' destruct(EQ') *
    239238  | ** #nxt' * #at_mid #_ #_ * #mid_other #_
Note: See TracChangeset for help on using the changeset viewer.