Ignore:
Timestamp:
Nov 22, 2010, 11:43:04 AM (10 years ago)
Author:
mulligan
Message:

More changes. Added datatype for addressing modes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/List.ma

    r247 r248  
    55include "Util.ma".
    66include "Universes.ma".
     7include "Bool.ma".
    78include "Nat.ma".
    89(* include "Maybe.ma". *)
     
    3940(* Lookup.                                                                    *)
    4041(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    41      
     42   
     43(*   
    4244nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝
    4345  match n with
     
    8486          ]
    8587    ].
     88*)
    8689   
    8790(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    205208    ].
    206209   
    207 nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l
    208   match l with
    209     [ Empty ⇒ False
     210nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool
     211  match l with
     212    [ Empty ⇒ cic:/matita/Cerco/Bool/Bool.con(0,2,0)
    210213    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
    211214    ].
     
    318321  nelim l.
    319322  nnormalize.
    320   napplyS append_empty_left_neutral.
     323  nrewrite > (append_empty_left_neutral ? ?).
     324  @.
    321325  #H L A.
    322326  nnormalize.
    323327  nrewrite > A.
    324   napplyS append_associative.
     328  nrewrite > (append_associative ? (reverse ? m) (reverse ? L) (Cons ? H (Empty ?))).
     329  @.
    325330nqed.
    326331
     
    378383  #H L H2.
    379384  nnormalize.
    380   //.
     385  nrewrite > H2.
     386  @.
    381387nqed.
    382388
     
    391397  #H L H2.
    392398  nnormalize.
    393   //.
    394 nqed.
    395 
     399  nrewrite > H2.
     400  @.
     401nqed.
     402
     403(*
    396404nlemma empty_get_index_nothing:
    397405  ∀A: Type[0].
     
    404412  //.
    405413nqed.
     414*)
    406415
    407416nlemma rotate_right_empty:
Note: See TracChangeset for help on using the changeset viewer.