Ignore:
Timestamp:
Nov 29, 2010, 11:17:58 AM (10 years ago)
Author:
mulligan
Message:

Got fold_right_i to type check. Moved eq_rect_Type0 into Plogic/equality.ma. Added new file for main processor execution loop.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Plogic/equality.ma

    r268 r328  
    3232 ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
    3333 #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
     34nqed.
     35
     36nlemma eq_rect_Type0_r :
     37  ∀A: Type[0].
     38  ∀a:A.
     39  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     40  #A a P H x p.
     41  ngeneralize in match H.
     42  ngeneralize in match P.
     43  ncases p.
     44  //.
    3445nqed.
    3546
Note: See TracChangeset for help on using the changeset viewer.