blob: 51f7c4dabcf86ec46f4c3a4e90c70d95767033d7 (
plain)
1
2
3
4
5
6
7
|
(* This example, checks the efficiency of the abstract machine used by ring *)
(* Expected time < 1.00s *)
Require Import ZArith.
Open Scope Z_scope.
Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
Timeout 5 Time intro; ring.
|
