diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-30 14:33:32 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-30 14:33:32 +0100 |
| commit | 702476dccbcad00bdbcaf2d0064384bde21d4d59 (patch) | |
| tree | f209582590720c666e2a947d4c40dc8666a7f7ff /examples | |
| parent | 6c02c60ee6c72bda1be390a60cae775c255d5dd6 (diff) | |
| download | smtcoq-702476dccbcad00bdbcaf2d0064384bde21d4d59.tar.gz smtcoq-702476dccbcad00bdbcaf2d0064384bde21d4d59.zip | |
gestion des symboles de fonction n-aires
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/examples/Example.v b/examples/Example.v index 60d1a2b..98175a2 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -137,6 +137,18 @@ Qed. Local Close Scope nat_scope. +(* An example with all 3 types and a binary function *) +Goal forall f : positive -> nat -> N, forall (x : positive) (y : nat), + implb (x =? 3)%positive + (implb (Nat.eqb y 7) + (implb (f 3%positive 7%nat =? 12)%N + (f x y =? 12)%N)) = true. +pos_convert. +nat_convert. +N_convert. +verit. +Qed. + Open Scope Z_scope. (* Some examples of using verit with lemmas. Use <verit_base H1 .. Hn; vauto> @@ -211,4 +223,4 @@ Section group. Proof. intro H. verit_base H; vauto. Qed. Clear_lemmas. -End group. +End group.
\ No newline at end of file |