Fix run test exhaustive_vm_impl_test

leanprover-community · May 14, 2020 · 7682053 · 7682053
1 parent 36afaaa
commit 7682053
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/tests/lean/run/exhaustive_vm_impl_test.lean b/tests/lean/run/exhaustive_vm_impl_test.lean
@@ -85,7 +85,6 @@ run_cmd verify $ ∀ x < 10, ∀ y < 10, is_ok $ nat.mul x y
 run_cmd verify $ ∀ x < 50, ∀ y < 50, is_ok $ nat.sub x y
 run_cmd verify $ ∀ x < 50, ∀ y < 50, is_ok $ nat.div x y
 run_cmd verify $ ∀ x < 100, ∀ y < 100, is_ok $ nat.mod x y
-run_cmd verify $ ∀ x < 100, ∀ y < 100, is_ok $ nat.gcd x y
 run_cmd verify $ ∀ x < 50, ∀ y < 50, is_ok $ nat.decidable_eq x y
 run_cmd verify $ ∀ x < 50, ∀ y < 50, is_ok $ nat.decidable_le x y
 run_cmd verify $ ∀ x < 50, ∀ y < 50, is_ok $ nat.decidable_lt x y
@@ -113,7 +112,6 @@ run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.mul x y
 run_cmd verify $ ∀ x ∈ ints, is_ok $ int.neg x
 run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.quot x y
 run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.rem x y
-run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.gcd x y
 run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.decidable_eq x y
 run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.decidable_le x y
 run_cmd verify $ ∀ x ∈ ints, ∀ y ∈ ints, is_ok $ int.decidable_lt x y