diff options
Diffstat (limited to 'test-suite/modules/fun_objects.v')
-rw-r--r-- | test-suite/modules/fun_objects.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v new file mode 100644 index 00000000..0f8eef84 --- /dev/null +++ b/test-suite/modules/fun_objects.v @@ -0,0 +1,32 @@ +Implicit Arguments On. + +Module Type SIG. + Parameter id:(A:Set)A->A. +End SIG. + +Module M[X:SIG]. + Definition idid := (X.id X.id). + Definition id := (idid X.id). +End M. + +Module N:=M. + +Module Nat. + Definition T := nat. + Definition x := O. + Definition id := [A:Set][x:A]x. +End Nat. + +Module Z:=(N Nat). + +Check (Z.idid O). + +Module P[Y:SIG] := N. + +Module Y:=P Nat Z. + +Check (Y.id O). + + + + |