diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/modules/Demo.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/modules/Demo.v')
-rw-r--r-- | test-suite/modules/Demo.v | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v new file mode 100644 index 00000000..1e9273f0 --- /dev/null +++ b/test-suite/modules/Demo.v @@ -0,0 +1,55 @@ +Module M. + Definition t:=nat. + Definition x:=O. +End M. + +Print M.t. + + +Module Type SIG. + Parameter t:Set. + Parameter x:t. +End SIG. + + +Module F[X:SIG]. + Definition t:=X.t->X.t. + Definition x:t. + Intro. + Exact X.x. + Defined. + Definition y:=X.x. +End F. + + +Module N := F M. + +Print N.t. +Eval Compute in N.t. + + +Module N' : SIG := N. + +Print N'.t. +Eval Compute in N'.t. + + +Module N'' <: SIG := F N. + +Print N''.t. +Eval Compute in N''.t. + +Eval Compute in N''.x. + + +Module N''' : SIG with Definition t:=nat->nat := N. + +Print N'''.t. +Eval Compute in N'''.t. + +Print N'''.x. + + +Import N'''. + +Print t.
\ No newline at end of file |