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

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r1410 r1516  
    139139  val_typ v' t'.
    140140#t #t' #op elim op
    141 [ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?)
    142   cases sg whd in ⊢ (??%? → ?) #E' destruct %
    143 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E' destruct %
     141[ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?);
     142  cases sg whd in ⊢ (??%? → ?); #E' destruct %
     143| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E' destruct %
    144144| #t'' #sz #sg cases t''
    145   [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?) %
     145  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
    146146  | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
    147     [ whd in ⊢ (??%? → ?) #E' destruct; %
    148     | #b #c #o whd in ⊢ (??%? → ?) #E' destruct %
     147    [ whd in ⊢ (??%? → ?); #E' destruct; %
     148    | #b #c #o whd in ⊢ (??%? → ?); #E' destruct %
    149149    ]
    150150  | #f *
    151151  ]
    152 | #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %
    153 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    154 | #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    155 | #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
    156 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
    157 | #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
    158 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
    159 | #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
    160 | #t'' #v #v' #H whd in ⊢ (??%? → ?) #E destruct @H
    161 | #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) cases (eq_bv ???)
    162   whd in ⊢ (??%? → ?) #E destruct //
     152| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %
     153| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     154| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     155| #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
     156| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
     157| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
     158| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     159| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
     160| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
     161| #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
     162  whd in ⊢ (??%? → ?); #E destruct //
    163163| #sz #sg #r #v #v' #H @(elim_val_typ … H) %
    164   [ whd in ⊢ (??%? → ?) #E destruct %
    165   | #b #c #o whd in ⊢ (??%? → ?) #E destruct
     164  [ whd in ⊢ (??%? → ?); #E destruct %
     165  | #b #c #o whd in ⊢ (??%? → ?); #E destruct
    166166  ]
    167167] qed.
Note: See TracChangeset for help on using the changeset viewer.