Changeset 2286 for src/ASM/Util.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2211 r2286  
    14371437interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
    14381438
     1439lemma If_elim : ∀A.∀P : A → Prop.∀b : bool.∀f : b → A.∀g : Not (bool_to_Prop b) → A.
     1440  (∀prf.P (f prf)) → (∀prf.P (g prf)) → P (If b then with prf do f prf else with prf do g prf).
     1441#A #P * #f #g #H1 #H2 normalize // qed.
     1442
    14391443(* Also extracts an equality proof (useful when not using Russell). *)
    14401444notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
Note: See TracChangeset for help on using the changeset viewer.