From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/success/Projection.v | 45 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 test-suite/success/Projection.v (limited to 'test-suite/success/Projection.v') diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v new file mode 100644 index 00000000..7f5cd800 --- /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. +*) -- cgit v1.2.3