diff options
Diffstat (limited to 'examples/switching_input.v')
| -rw-r--r-- | examples/switching_input.v | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/examples/switching_input.v b/examples/switching_input.v deleted file mode 100644 index 629a3ad..0000000 --- a/examples/switching_input.v +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2019 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -Require Import SMTCoq. -Require Import Bool. -Local Open Scope int63_scope. - -Parameter m : Z -> Z. -Axiom m_0 : m 0 =? 5. - -Lemma cinq_m_0 : - m 0 =? 5. -Proof. verit_base m_0; vauto. Qed. |