diff options
| author | Pierre-Marie Pédrot | 2017-07-31 22:07:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-01 00:25:48 +0200 |
| commit | f9e7c43b5884f5231f14ec7b008b1eb660026a0e (patch) | |
| tree | 6e47ac2d122e932ae429b9eb684d3c32f018bec1 /tests/example2.v | |
| parent | 0f72b089de52ad7d26d71e56003b140fa5012635 (diff) | |
Adding new scopes for standard Ltac structures.
Diffstat (limited to 'tests/example2.v')
| -rw-r--r-- | tests/example2.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v new file mode 100644 index 0000000000..14a6b68e18 --- /dev/null +++ b/tests/example2.v @@ -0,0 +1,15 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Notation "split" bnd(bindings) := Std.split (bnd ()). + +Goal exists n, n = 0. +Proof. +split with (x := 0). +Std.reflexivity (). +Qed. + +Goal exists n, n = 0. +Proof. +split with 0. +split. +Qed. |