diff options
Diffstat (limited to 'test-suite/modules/Demo.v')
| -rw-r--r-- | test-suite/modules/Demo.v | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v index 1e9273f0..1f27fe1b 100644 --- a/test-suite/modules/Demo.v +++ b/test-suite/modules/Demo.v @@ -1,51 +1,51 @@ Module M. - Definition t:=nat. - Definition x:=O. + Definition t := nat. + Definition x := 0. End M. Print M.t. Module Type SIG. - Parameter t:Set. - Parameter x:t. + 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. +Module F (X: SIG). + Definition t := X.t -> X.t. + Definition x : t. + intro. + exact X.x. Defined. - Definition y:=X.x. + Definition y := X.x. End F. Module N := F M. Print N.t. -Eval Compute in N.t. +Eval compute in N.t. Module N' : SIG := N. Print N'.t. -Eval Compute in N'.t. +Eval compute in N'.t. Module N'' <: SIG := F N. Print N''.t. -Eval Compute in N''.t. +Eval compute in N''.t. -Eval Compute in N''.x. +Eval compute in N''.x. -Module N''' : SIG with Definition t:=nat->nat := N. +Module N''' : SIG with Definition t := nat -> nat := N. Print N'''.t. -Eval Compute in N'''.t. +Eval compute in N'''.t. Print N'''.x. |