Changeset 1094 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 28, 2011, 5:26:06 PM (8 years ago)
Author:
mulligan
Message:

some changes from today to do with liveness analyses

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1075 r1094  
    3232  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    3333  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     34  ].
     35
     36let rec prefix
     37  (A: Type[0]) (k: nat) (l: list A)
     38    on l ≝
     39  match l with
     40  [ nil ⇒ [ ]
     41  | cons hd tl ⇒
     42    match k with
     43    [ O ⇒ [ ]
     44    | S k' ⇒ hd :: prefix A k' tl
     45    ]
    3446  ].
    3547 
Note: See TracChangeset for help on using the changeset viewer.