diff options
Diffstat (limited to 'test-suite/modules/Tescik.v')
| -rw-r--r-- | test-suite/modules/Tescik.v | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v index 13c28418..8dadace7 100644 --- a/test-suite/modules/Tescik.v +++ b/test-suite/modules/Tescik.v @@ -1,30 +1,30 @@ Module Type ELEM. - Parameter A:Set. - Parameter x:A. + Parameter A : Set. + Parameter x : A. End ELEM. Module Nat. - Definition A:=nat. - Definition x:=O. + Definition A := nat. + Definition x := 0. End Nat. -Module List[X:ELEM]. - Inductive list : Set := nil : list - | cons : X.A -> list -> list. +Module List (X: ELEM). + Inductive list : Set := + | nil : list + | cons : X.A -> list -> list. - Definition head := - [l:list]Cases l of - nil => X.x - | (cons x _) => x - end. + Definition head (l : list) := match l with + | nil => X.x + | cons x _ => x + end. - Definition singl := [x:X.A] (cons x nil). + Definition singl (x : X.A) := cons x nil. - Lemma head_singl : (x:X.A)(head (singl x))=x. - Auto. + Lemma head_singl : forall x : X.A, head (singl x) = x. + auto. Qed. End List. -Module N:=(List Nat). +Module N := List Nat.
\ No newline at end of file |