From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/modules/Tescik.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 test-suite/modules/Tescik.v (limited to 'test-suite/modules/Tescik.v') diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v new file mode 100644 index 00000000..13c28418 --- /dev/null +++ b/test-suite/modules/Tescik.v @@ -0,0 +1,30 @@ + +Module Type ELEM. + Parameter A:Set. + Parameter x:A. +End ELEM. + +Module Nat. + Definition A:=nat. + Definition x:=O. +End Nat. + +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 singl := [x:X.A] (cons x nil). + + Lemma head_singl : (x:X.A)(head (singl x))=x. + Auto. + Qed. + +End List. + +Module N:=(List Nat). -- cgit v1.2.3