diff options
| -rw-r--r-- | test-suite/success/implicit.v | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 5f0067412c..bd74742857 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,9 +1,18 @@ (* Implicit on section variables *) -(* Example submitted by David Nowak *) Set Implicit Arguments. + +(* Example submitted by David Nowak *) + Section Spec. Variable A:Set. Variable op : (A:Set)A->A->Set. Infix 6 "#" op. Check (x:A)(x # x). + +(* Example submitted by Christine *) +Record stack : Type := {type : Set; elt : type; + empty : type -> bool; proof : (empty elt)=true }. + +Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack. + |