diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-15 13:39:08 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-22 11:07:08 +0200 |
commit | a9dc951e9068b18ee1cf0e51b2c4ae7a7c40354a (patch) | |
tree | a1a4073e5cab0d9af97c129a1574b0549464cc6d /test-suite/ssr | |
parent | 7721aeeede9c5578f29e7f37a5ea2005c7d9ce1b (diff) |
[ssr] implement {}/v as a short hand for {v}/v when v is an id
Diffstat (limited to 'test-suite/ssr')
-rw-r--r-- | test-suite/ssr/ipat_clear_if_id.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v new file mode 100644 index 000000000..7a44db2ea --- /dev/null +++ b/test-suite/ssr/ipat_clear_if_id.v @@ -0,0 +1,23 @@ +Require Import ssreflect. + +Axiom v1 : nat -> bool. + +Section Foo. + +Variable v2 : nat -> bool. + +Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True. +Proof. +move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4. +Check b1 : bool. +Check b2 : bool. +Check b3 : bool. +Check b4 : bool. +Fail Check v3. +Fail Check v4. +Fail Check v5. +Check v2 : nat -> bool. +by []. +Qed. + +End Foo. |