Changeset 1519 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 21, 2011, 12:10:57 PM (8 years ago)
Author:
campbell
Message:

More syntax updates.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1515 r1519  
    4040   # H2
    4141   normalize
    42    change in H2: (??%?) with (orb ??)
     42   change in H2: (??%?); with (orb ??)
    4343   cases (inclusive_disjunction_true … H2)
    4444   [ # K
     
    7777   # tl
    7878   # II
    79    whd in ⊢ (% → ? → ?)
     79   whd in ⊢ (% → ? → ?);
    8080   lapply (refl … (is_in … (he:::tl) a))
    81    cases (is_in … (he:::tl) a) in ⊢ (???% → %)
     81   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
    8282   [ # K
    8383     # _
    8484     normalize in K;
    85      whd in ⊢ (% → ?)
    86      lapply (refl … (subvector_with … eq_a (he:::tl) q))
    87      cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
     85     whd in ⊢ (% → ?);
     86     lapply (refl … (subvector_with … eq_a (he:::tl) q));
     87     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
    8888     [ # K1
    8989       # _
    90        change in K1 with ((andb ? (subvector_with …)) = true)
     90       change in K1; with ((andb ? (subvector_with …)) = true)
    9191       cases (conjunction_true … K1)
    9292       # K3
     
    105105     | # K1
    106106       # K2
    107        (normalize in K2)
     107       (normalize in K2;)
    108108       cases K2;
    109109     ]
Note: See TracChangeset for help on using the changeset viewer.