Changeset 2767 for src/utilities


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.

Location:
src/utilities
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extranat.ma

    r2670 r2767  
    11include "basics/types.ma".
    22include "arithmetics/nat.ma".
     3include "utilities/option.ma".
     4
     5(* JHM: here, for definiteness; used in ASM/ASM.ma *)
     6let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝
     7match N return λy. option (n < y) with
     8[ O ⇒ None ?
     9| S N' ⇒
     10    match n return λx. option (x < S N') with
     11    [ O ⇒ (return (lt_O_S ?))
     12    | S n' ⇒ (! prf ← nat_bound_opt N' n' ; return (le_S_S ?? prf))
     13    ]
     14].
    315
    416inductive nat_compared : nat → nat → Type[0] ≝
  • 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.