Changeset 998 for src/ASM/Vector.ma


Ignore:
Timestamp:
Jun 20, 2011, 5:05:23 PM (9 years ago)
Author:
sacerdot
Message:

Half repaired, half broken. Most functions no longer return option types,
taking in input dependent types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r961 r998  
    170170 split' A m n v.
    171171
    172 
    173172definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
    174173  λA: Type[0].
     
    306305   
    307306interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
     307
     308axiom split_elim':
     309  ∀A: Type[0].
     310  ∀B: Type[1].
     311  ∀l, m, v.
     312  ∀T: Vector A l → Vector A m → B.
     313  ∀P: B → Prop.
     314    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
     315      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
     316
     317axiom split_elim'':
     318  ∀A: Type[0].
     319  ∀B,B': Type[1].
     320  ∀l, m, v.
     321  ∀T: Vector A l → Vector A m → B.
     322  ∀T': Vector A l → Vector A m → B'.
     323  ∀P: B → B' → Prop.
     324    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
     325      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
     326        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
    308327   
    309328let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.