Ignore:
Timestamp:
Nov 23, 2010, 2:30:10 PM (11 years ago)
Author:
sacerdot
Message:
  • Minimal changes to make it compile with the standard distribution of Matita once this directory is substituted to nlibrary
  • ambiguity reduced by lower-casing booleans
File:
1 edited

Legend:

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

    r256 r260  
    88include "Nat.ma".
    99(* include "Maybe.ma". *)
    10 include "Equality.ma".
     10include "Plogic/equality.ma".
    1111
    1212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    136136    | Cons hd tl ⇒
    137137      match f hd a with
    138         [ True ⇒ (reverse A b) @ tl
    139         | False ⇒ remove_first_with_aux A f a tl (hd :: b)
     138        [ true ⇒ (reverse A b) @ tl
     139        | false ⇒ remove_first_with_aux A f a tl (hd :: b)
    140140        ]
    141141    ].
     
    154154    | Cons hd tl ⇒
    155155      match f hd a with
    156         [ True ⇒ remove_all_with_aux A f a tl b
    157         | False ⇒ remove_all_with_aux A f a tl (hd :: b)
     156        [ true ⇒ remove_all_with_aux A f a tl b
     157        | false ⇒ remove_all_with_aux A f a tl (hd :: b)
    158158        ]
    159159    ].
     
    171171    | Cons hd tl ⇒
    172172      match f hd with
    173         [ True ⇒ drop_while A f tl
    174         | False ⇒ Cons A hd tl
     173        [ true ⇒ drop_while A f tl
     174        | false ⇒ Cons A hd tl
    175175        ]
    176176    ].
     
    203203    | Cons hd tl ⇒
    204204      match f hd with
    205         [ True ⇒ hd :: (filter A f tl)
    206         | False ⇒ filter A f tl
     205        [ true ⇒ hd :: (filter A f tl)
     206        | false ⇒ filter A f tl
    207207        ]
    208208    ].
     
    210210nlet rec member_with (A: Type[0]) (a: A) (f: A → A → Bool) (l: List A) on l: Bool ≝
    211211  match l with
    212     [ Empty ⇒ cic:/matita/Cerco/Bool/Bool.con(0,2,0)
     212    [ Empty ⇒ false
    213213    | Cons hd tl ⇒ inclusive_disjunction (f hd a) (member_with A a f tl)
    214214    ].
     
    219219    | Cons hd tl ⇒
    220220      match member_with A hd f tl with
    221         [ True ⇒ nub_with A f tl
    222         | False ⇒ hd :: (nub_with A f tl)
     221        [ true ⇒ nub_with A f tl
     222        | false ⇒ hd :: (nub_with A f tl)
    223223        ]
    224224    ].
     
    257257    | Cons hd tl ⇒
    258258      match member_with A hd f m with
    259         [ True ⇒ hd :: (intersection_with A f tl m)
    260         | False ⇒ intersection_with A f tl m
     259        [ true ⇒ hd :: (intersection_with A f tl m)
     260        | false ⇒ intersection_with A f tl m
    261261        ]
    262262    ].
Note: See TracChangeset for help on using the changeset viewer.