diff options
author | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 17:06:03 +0000 |
---|---|---|
committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 17:08:26 +0000 |
commit | 420b38cba7aedfcfeac5671a7db0c02c4bb14a0c (patch) | |
tree | 688c9c61de37e2a16ddc87fc91272e80338eaae1 /test-suite/success | |
parent | cda674b91ec137bb4c995063888cc5059884ac8c (diff) |
[test suite] Test case for attributes
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/attribute-syntax.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v new file mode 100644 index 000000000..83fb3d0c8 --- /dev/null +++ b/test-suite/success/attribute-syntax.v @@ -0,0 +1,23 @@ +From Coq Require Program. + +Section Scope. + +#[local] Coercion nat_of_bool (b: bool) : nat := + if b then 0 else 1. + +Check (refl_equal : true = 0 :> nat). + +End Scope. + +Fail Check 0 = true :> nat. + +#[polymorphic] +Definition ι T (x: T) := x. + +Check ι _ ι. + +#[program] +Fixpoint f (n: nat) {wf lt n} : nat := _. + +#[deprecated(since="8.9.0")] +Ltac foo := foo. |