blob: 2d585ce5c5be41c86c018b3f8bb10836c9309019 (
plain)
1
2
3
4
5
6
7
8
|
(* 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.
Abort.
|
