Changeset 2032 for src/ASM/Util.ma


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2005 r2032  
    172172qed.
    173173
    174 let rec split
     174let rec safe_split
    175175  (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|)
    176176    on index ≝
     
    181181    [ nil ⇒ λnil_absrd. ?
    182182    | cons hd tl ⇒ λcons_prf.
    183       let 〈l1, l2〉 ≝ split A tl index' ? in
     183      let 〈l1, l2〉 ≝ safe_split A tl index' ? in
    184184        〈hd :: l1, l2〉
    185185    ] succ_prf
Note: See TracChangeset for help on using the changeset viewer.