From 40f44123d496b63ce6cfc6df3198ba98bd4bba8f Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 28 Nov 2003 14:10:55 +0000 Subject: Simplest Demo on modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5014 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/modules/Demo.v | 55 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 test-suite/modules/Demo.v (limited to 'test-suite/modules') diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v new file mode 100644 index 000000000..1e9273f07 --- /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 -- cgit v1.2.3