Changeset 2042


Ignore:
Timestamp:
Jun 8, 2012, 11:33:18 PM (5 years ago)
Author:
sacerdot
Message:

Repaired (Type => DeqSet?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r1949 r2042  
    176176*)
    177177
     178definition unit_deqset: DeqSet ≝ mk_DeqSet unit (λ_.λ_.true) ?.
     179 * * /2/
     180qed.
     181
    178182definition block_cont_in_code : ∀p,g.codeT p g → ∀ty.
    179   code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit → Prop ≝
     183  code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit_deqset → Prop ≝
    180184  λp,g.λc : codeT p g.λty,src,b,dst.
    181185  ∃mid.seq_list_in_code p g c src (\fst b) mid ∧
    182186  match ty
    183187  return λx.stmt_type_if ? x ??? →
    184     stmt_type_if ? x ?? → Prop
     188    stmt_type_if ? x ? unit_deqset → Prop
    185189  with
    186190  [ SEQ ⇒ λs,dst.
Note: See TracChangeset for help on using the changeset viewer.