Ignore:
Timestamp:
Mar 4, 2011, 6:20:26 PM (9 years ago)
Author:
campbell
Message:

A few definitions that will be useful for some preliminary rtlabs semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/cerco/Vector.ma

    r535 r636  
    201201    ].
    202202
     203let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
     204                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
     205  match v with
     206    [ VEmpty ⇒ x
     207    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
     208    ].
     209
    203210let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
    204211                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.