Changeset 1519 for src/ASM/Interpret.ma

Timestamp:

Nov 21, 2011, 12:10:57 PM (8 years ago)

Author:

campbell

Message:

More syntax updates.

File:

• src/ASM/Interpret.ma (modified) (3 diffs)

src/ASM/Interpret.ma

@@ -40 +40 @@
    # H2
    normalize
-   change in H2: (??%?) with (orb ??)
+   change in H2: (??%?); with (orb ??)
    cases (inclusive_disjunction_true … H2)
    [ # K
@@ -77 +77 @@
    # tl
    # II
-   whd in ⊢ (% → ? → ?)
+   whd in ⊢ (% → ? → ?);
    lapply (refl … (is_in … (he:::tl) a))
-   cases (is_in … (he:::tl) a) in ⊢ (???% → %)
+   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
    [ # K
      # _
      normalize in K;
-     whd in ⊢ (% → ?)
-     lapply (refl … (subvector_with … eq_a (he:::tl) q))
-     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %)
+     whd in ⊢ (% → ?);
+     lapply (refl … (subvector_with … eq_a (he:::tl) q));
+     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
      [ # K1
        # _
-       change in K1 with ((andb ? (subvector_with …)) = true)
+       change in K1; with ((andb ? (subvector_with …)) = true)
        cases (conjunction_true … K1)
        # K3
@@ -105 +105 @@
      | # K1
        # K2
-       (normalize in K2)
+       (normalize in K2;)
        cases K2;
      ]