diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-12 12:27:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-30 14:40:45 +0200 |
| commit | 3074967fd01acc5987eb2ea648fcfe32aeca1749 (patch) | |
| tree | 1620335417ff4fb026b151239b3aa643d9c97aad /test-suite/success/forward.v | |
| parent | be73d7eccd3e3165ce719b36910920e05cf416bc (diff) | |
Few tests for e-variants of assert, set, remember.
Diffstat (limited to 'test-suite/success/forward.v')
| -rw-r--r-- | test-suite/success/forward.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v new file mode 100644 index 000000000..0ed5b524f --- /dev/null +++ b/test-suite/success/forward.v @@ -0,0 +1,18 @@ +(* Testing forward reasoning *) + +Goal 0=0. +Fail assert (_ = _). +eassert (_ = _)by reflexivity. +eassumption. +Qed. + +Goal 0=0. +Fail set (S ?[nl]). +eset (S ?[n]). +remember (S ?n) as x. +instantiate (n:=0). +Fail remember (S (S _)). +eremember (S (S ?[x])). +instantiate (x:=0). +reflexivity. +Qed. |