diff options
Diffstat (limited to 'unit-tests')
-rw-r--r-- | unit-tests/Tests_verit_tactics.v | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index a6ea27b..4285f96 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1498,3 +1498,67 @@ Section OCamlCompDec. x ++ y = a0::nil -> x = nil /\ y = a0::nil \/ x = a0::nil /\ y = nil. Proof. verit_no_check. Qed. End OCamlCompDec. + + +Section TimeoutBool. + Variable P : Z -> bool. + Variable H0 : P 0. + Variable HInd : forall n, implb (P n) (P (n + 1)). + + Goal P 3. + Proof. + verit_bool_base_auto_timeout (Some (H0, HInd)) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_no_check_base_auto_timeout (Some (H0, HInd)) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_timeout 10. + Qed. + + Goal P 3. + Proof. + verit_bool_no_check_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_bool_no_check_timeout 10. + Qed. +End TimeoutBool. + + +Section TimeoutProp. + Variable P : Z -> bool. + Variable H0 : P 0. + Variable HInd : forall n, (P n) -> (P (n + 1)). + + Goal P 3. + Proof. + verit_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_timeout 10. + Qed. + + Goal P 3. + Proof. + verit_no_check_timeout (H0, HInd) 10. + Qed. + + Goal P 3. + Proof. + verit_no_check_timeout 10. + Qed. +End TimeoutProp. |