Changeset 1350 for src/utilities


Ignore:
Timestamp:
Oct 11, 2011, 2:27:53 AM (8 years ago)
Author:
sacerdot
Message:

Porting to latest destruct tactic.

Note: the tactics has a few remaining bugs to be ironed out.
Look for "Wilmer: XXX" comments in the .ma files to see where
these are avoided ATM using axioms.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1338 r1350  
    522522 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
    523523#m #n @(pos_cases … n)
    524 [ >(divide_by_one m) #dv #md #H destruct /2/
     524[ >(divide_by_one m) #dv #md #H destruct normalize /2/
    525525| #n' elim m;
    526526  [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/
     
    540540          lapply (partial_minus_to_Prop md'' n);
    541541          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
    542           #lt #e destruct % [ /3/ | *: /2/ ] @plt_pos
     542          #lt #e destruct % [ normalize /3/ | *: normalize /2/ ] @plt_pos
    543543          [ 1,3,5,7: @double_lt1 /2/;
    544544          | 2,4: @double_lt3 /2/;
Note: See TracChangeset for help on using the changeset viewer.