Ignore:
Timestamp:
Mar 3, 2013, 2:03:58 PM (7 years ago)
Author:
mckinna
Message:

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/option.ma

    r1976 r2767  
    8383lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
    8484  ≝ m_pred_mp ….
     85 
     86(* moved from ASM/ASM.ma! *)
     87definition partial_injection : ∀A,B.(A → option B) → Prop ≝
     88λA,B,f.∀x,y,z.f x = Some ? z → f y = Some ? z → x = y.
Note: See TracChangeset for help on using the changeset viewer.