Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r1515 r1516  
    6262[ * //
    6363| #tl #IH *
    64   [ whd in ⊢ (??%%) @IH
     64  [ whd in ⊢ (??%%); @IH
    6565  | #x #l #r @IH
    6666  ]
    6767| #tl #IH *
    68   [ whd in ⊢ (??%%) @IH
     68  [ whd in ⊢ (??%%); @IH
    6969  | #x #l #r @IH
    7070  ]
     
    8080| #b' #IH *
    8181  [ * [ #NE @refl | #x #l #r #NE @refl ]
    82   | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
    83           | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
     82  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     83          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
    8484          ]
    8585  | #c' * //
     
    8888  [ * [ #NE @refl | #x #l #r #NE @refl ]
    8989  | #c' * //
    90   | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
    91           | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
     90  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
     91          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
    9292          ]
    9393  ]
     
    110110[ * [ // | * // #x #l #r normalize #E destruct ]
    111111| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
    112                    cases (update A b' a r) in U ⊢ %
     112                   cases (update A b' a r) in U ⊢ %;
    113113                   [ // | normalize #t #E destruct ]
    114114            ]
    115115| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
    116                    cases (update A b' a l) in U ⊢ %
     116                   cases (update A b' a l) in U ⊢ %;
    117117                   [ // | normalize #t #E destruct ]
    118118            ]
     
    124124#A #b #a elim b
    125125[ * [ #t' normalize #E destruct
    126     | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?)
     126    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
    127127      #E destruct //
    128128    ]
    129129| #b' #IH *
    130130  [ #t' normalize #E destruct
    131   | #x #l #r #t' whd in ⊢ (??%? → ??%?)
     131  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    132132    lapply (IH r)
    133133    cases (update A b' a r)
     
    138138| #b' #IH *
    139139  [ #t' normalize #E destruct
    140   | #x #l #r #t' whd in ⊢ (??%? → ??%?)
     140  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
    141141    lapply (IH l)
    142142    cases (update A b' a l)
Note: See TracChangeset for help on using the changeset viewer.