diff options
Diffstat (limited to 'coq/ex-module.v')
| -rw-r--r-- | coq/ex-module.v | 40 |
1 files changed, 34 insertions, 6 deletions
diff --git a/coq/ex-module.v b/coq/ex-module.v index f8df0c31..227b3ff7 100644 --- a/coq/ex-module.v +++ b/coq/ex-module.v @@ -1,4 +1,27 @@ +Module Type O1. +Parameter A:Set. +Parameter B:Set. +End O1. + + +Module R:O1. +Definition A:=nat. +Definition B:=bool. +End R. + +Module R2: O1 with Definition A:=nat. +Definition A:=nat. +Definition B:=bool. +End R2. + +Module R4. +Module R3: O1 with Definition A:=nat :=R2. +End R4. + + + + Module M. Module Type SIG. Parameter T:Set. @@ -15,6 +38,10 @@ Module M. Module O:=N. End M. +Import M. +Print t. + + Definition t:O=O. Trivial. Save. @@ -24,13 +51,14 @@ Section toto. Print M. End toto. - Module N:=M. +Module N:=M. + + +Module Type typ. +Parameter T:Set. +Parameter a:T. +End typ. -Module R:N.SIG. - Definition T:Set:=nat. - Definition x:T:= O. - Definition foo:nat:=(S O). -End R. Module Type N'. |