diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /examples/Non_terminating.v | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'examples/Non_terminating.v')
| -rw-r--r-- | examples/Non_terminating.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/examples/Non_terminating.v b/examples/Non_terminating.v new file mode 100644 index 0000000..087301a --- /dev/null +++ b/examples/Non_terminating.v @@ -0,0 +1,11 @@ +Require Import SMTCoq. + +Parameter g : Z -> Z. + +Axiom g_2_linear : forall x, Zeq_bool (g (x + 1)) ((g x) + 2). + +Lemma apply_lemma_multiple : + forall x y, Zeq_bool (g (x + y)) ((g x) + y * 2). + +Proof. + verit g_2_linear. |