From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- test-suite/modules/Tescik.v | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'test-suite/modules/Tescik.v') 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 -- cgit v1.2.3