diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 17:00:41 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 17:00:41 +0000 |
commit | ed9f35dd30e87038bb2333a7fa9b7ff75ecb1335 (patch) | |
tree | a273ae7b82790e413848f2d04ad86514c2dfc25c /coq/ex-module.v | |
parent | 2a8f91fc3c959ff96a583326815b57e54d262e90 (diff) |
Use official indentation\!
Diffstat (limited to 'coq/ex-module.v')
-rw-r--r-- | coq/ex-module.v | 51 |
1 files changed, 26 insertions, 25 deletions
diff --git a/coq/ex-module.v b/coq/ex-module.v index 2fbdbcf5..af2e4a08 100644 --- a/coq/ex-module.v +++ b/coq/ex-module.v @@ -10,7 +10,8 @@ Module R:O1. Definition B:=bool. End R. -Module R2: O1 with Definition A:=nat. +Module R2: O1 with + Definition A:=nat. Definition A:=nat. Definition B:=bool. End R2. @@ -69,28 +70,28 @@ Module Type N'. Definition T:=nat. Definition x:=O. End N''. - + Declare Module N':M.SIG. (* no interactive def started *) - Declare Module N''':= N'. (* no interactive def started *) - Declare Module N''''. (* interactive def started *) - Parameter foo:nat. - End N''''. (* interactive def ended *) -End N'. - - - -Lemma titi : O=O. - Trivial. - Module Type K:=N'. - Module N''':=M. -Save. - -(* Here is a bug of Coq: *) - -Lemma bar:O=O. - Module Type L. (* This should not be allowed by Coq, since the End L. below fails *) - Axiom foo: O=O. - End L. (* fails --> if we go back to Module Type: unsync *) - Module I. -End I. - + Declare Module N''':= N'. (* no interactive def started *) + Declare Module N''''. (* interactive def started *) + Parameter foo:nat. + End N''''. (* interactive def ended *) + End N'. + + + + Lemma titi : O=O. + Trivial. + Module Type K:=N'. + Module N''':=M. + Save. + + (* Here is a bug of Coq: *) + + Lemma bar:O=O. + Module Type L. (* This should not be allowed by Coq, since the End L. below fails *) + Axiom foo: O=O. + End L. (* fails --> if we go back to Module Type: unsync *) + Module I. + End I. + |