diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-03 07:24:27 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-03 07:24:27 +0000 |
commit | 14b7ce42bfe1a8934a8fd106d3d9610b6c41e041 (patch) | |
tree | 0e3e338dd45a88425f56084472ee4c211ec526a6 /test-suite/success/Projection.v | |
parent | 71d22a0cfa99a3c28e59c97e2d3ae68b08c4c47a (diff) |
Projections
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4298 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Projection.v')
-rw-r--r-- | test-suite/success/Projection.v | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v new file mode 100644 index 000000000..7f5cd8000 --- /dev/null +++ b/test-suite/success/Projection.v @@ -0,0 +1,45 @@ +Structure S : Type := + {Dom : Type; + Op : Dom -> Dom -> Dom}. + +Check [s:S](Dom s). +Check [s:S](Op s). +Check [s:S;a,b:(Dom s)](Op s a b). + +(* v8 +Check fun s:S => s.(Dom). +Check fun s:S => s.(Op). +Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b. +*) + +Set Implicit Arguments. +Unset Strict Implicits. + +Structure S' [A:Set] : Type := + {Dom' : Type; + Op' : A -> Dom' -> Dom'}. + +Check [s:(S' nat)](Dom' s). +Check [s:(S' nat)](Op' 2!s). +Check [s:(S' nat)](!Op' nat s). +Check [s:(S' nat);a:nat;b:(Dom' s)](Op' a b). +Check [s:(S' nat);a:nat;b:(Dom' s)](!Op' nat s a b). + +(* v8 +Check fun s:S' => s.(Dom'). +Check fun s:S' => s.(Op'). +Check fun (s:S') (a b:s.(Dom')) => _.(Op') a b. +Check fun (s:S') (a b:s.(Dom')) => s.(Op') a b. + +Set Implicit Arguments. +Unset Strict Implicits. + +Structure S' (A:Set) : Type := + {Dom' : Type; + Op' : A -> Dom' -> Dom'}. + +Check fun s:S' nat => s.(Dom'). +Check fun s:S' nat => s.(Op'). +Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => _.(@Op' nat) a b. +Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => s.(Op') a b. +*) |