diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/implicit.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/implicit.v')
-rw-r--r-- | test-suite/success/implicit.v | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index c597f9bf..1786424e 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,20 +1,23 @@ (* Implicit on section variables *) Set Implicit Arguments. +Unset Strict Implicit. (* Example submitted by David Nowak *) Section Spec. -Variable A:Set. -Variable op : (A:Set)A->A->Set. -Infix 6 "#" op V8only (at level 70). -Check (x:A)(x # x). +Variable A : Set. +Variable op : forall A : Set, A -> A -> Set. +Infix "#" := op (at level 70). +Check (forall x : A, x # x). (* Example submitted by Christine *) -Record stack : Type := {type : Set; elt : type; - empty : type -> bool; proof : (empty elt)=true }. +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. +Check + (forall (type : Set) (elt : type) (empty : type -> bool), + empty elt = true -> stack). End Spec. @@ -22,10 +25,10 @@ End Spec. 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 (fun x => fst (f x)). +Check (fun x => fst (f x)). +Notation rhs := snd. +Check (fun x => snd (f x)). (* V8 seulement Check (fun x => @ rhs ? ? (f x)). *) |