diff options
| -rw-r--r-- | test-suite/success/implicit.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 00230bfc46..9f2837e373 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -17,3 +17,13 @@ Record stack : Type := {type : Set; elt : type; Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack. End Spec. + +(* Example submitted by Frédéric (interesting in v8 syntax) *) + +Parameter f : nat -> nat * nat. +Notation lhs := fst. +Check [x](lhs ? ? (f x)). +Check [x](!lhs ? ? (f x)). +Notation "'rhs'" := snd. +Check [x](rhs ? ? (f x)). +Check [x](!rhs ? ? (f x)). |