Ignore:
Timestamp:
Mar 28, 2013, 7:49:22 PM (7 years ago)
Author:
campbell
Message:

Make a couple of tests monadic for easier inversion.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2728 r3022  
    626626] qed.
    627627
     628
     629definition check_cost_program_prf : ∀p:RTLabs_program. res (well_cost_labelled_program p) ≝
     630λp. (match check_cost_program p return λb. bool_to_Prop b ↔ well_cost_labelled_program p → res ? with
     631     [ true ⇒ λH. OK ??
     632     | false ⇒ λ_. Error ? (msg BadCostLabelling)
     633     ])
     634    (check_cost_program_ok p).
     635@(proj1 … H)
     636% qed.
     637
Note: See TracChangeset for help on using the changeset viewer.