Changeset 2767 for src/utilities
 Timestamp:
 Mar 3, 2013, 2:03:58 PM (7 years ago)
 Location:
 src/utilities
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/extranat.ma
r2670 r2767 1 1 include "basics/types.ma". 2 2 include "arithmetics/nat.ma". 3 include "utilities/option.ma". 4 5 (* JHM: here, for definiteness; used in ASM/ASM.ma *) 6 let rec nat_bound_opt (N:nat) (n:nat) : option (n < N) ≝ 7 match 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 ]. 3 15 4 16 inductive nat_compared : nat → nat → Type[0] ≝ 
src/utilities/option.ma
r1976 r2767 83 83 lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o 84 84 ≝ m_pred_mp …. 85 86 (* moved from ASM/ASM.ma! *) 87 definition 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.