diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:01:15 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:01:15 +0200 |
commit | 65c185275f8c78908c1496c6665bc7fd50a4607b (patch) | |
tree | 3d68caf8b482563c01ada2cf426f7f96d6fda76a /unit-tests | |
parent | deb9927455bcb3b506d17a63a9b7b5ec11fe9027 (diff) | |
download | smtcoq-65c185275f8c78908c1496c6665bc7fd50a4607b.tar.gz smtcoq-65c185275f8c78908c1496c6665bc7fd50a4607b.zip |
Clean-up
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. |