Changeset 1516 for src/joint/BEValues.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/BEValues.ma
r1395 r1516 74 74 [ O ⇒ λ_.[] 75 75 | 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. 77 77 78 78 definition bevals_of_pointer: pointer → list beval ≝ … … 84 84 * * #pbl #pok #poff 85 85 try % 86 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %]87 whd in ⊢ (??%?) >reflexive_eq_pointer >(eqb_n_n 2) %86 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 1) [2,3: %] 87 whd in ⊢ (??%?); >reflexive_eq_pointer >(eqb_n_n 2) % 88 88 qed. 89 89
Note: See TracChangeset
for help on using the changeset viewer.