Changeset 1516 for src/joint/BEValues.ma


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/joint/BEValues.ma

    r1395 r1516  
    7474  [ O ⇒ λ_.[]
    7575  | S m ⇒ λpr':n=S m.(BVptr p (mk_part … part …))::bevals_of_pointer_aux p (S part) m ?] (refl ? n).
    76 /3/ qed.
     76/3/ (*Andrea: by _ cannot be re-parsed*) qed.
    7777
    7878definition bevals_of_pointer: pointer → list beval ≝
     
    8484* * #pbl #pok #poff
    8585try %
    86 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
    87 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 2) %
     86whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]
     87whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) %
    8888qed.
    8989
Note: See TracChangeset for help on using the changeset viewer.