Changeset 1646 for src/ASM/Vector.ma


Ignore:
Timestamp:
Jan 16, 2012, 3:04:14 PM (8 years ago)
Author:
mulligan
Message:

finished the block_costs computation, and propagated the changes forward, subject to closing two axioms (an elimination principle, and a lemma on subvectors). moved some code around to its rightful place.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r1599 r1646  
    522522  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
    523523
    524 
    525 definition subvector_with ≝
    526   λA: Type[0].
    527   λn: nat.
    528   λm: nat.
    529   λf: A → A → bool.
    530   λv: Vector A n.
    531   λq: Vector A m.
    532     fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
     524let rec subvector_with
     525  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
     526    on sub: bool ≝
     527  match sub with
     528  [ VEmpty         ⇒ true
     529  | VCons n' hd tl ⇒
     530    if mem … eq … sup hd then
     531      subvector_with … eq tl sup
     532    else
     533      false
     534  ].
    533535   
    534536(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.