From: matitaweb Date: Wed, 16 Nov 2011 12:45:15 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=60610b9013095e8e3f060ad3ab24e62902757d91;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 76065b6db..fd0f71144 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -107,6 +107,8 @@ inductive pitem (S: a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"Alp definition pre ≝ λS.a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S a title="Product" href="cic:/fakeuri.def(1)"×/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"bool/a. +definition test ≝ λS:Alpha.λe: pre S. match e with [mk_pair i b ⇒ e]. + interpretation "pstar" 'kstar a = (pstar ? a). interpretation "por" 'plus a b = (por ? a b). interpretation "pcat" 'concat a b = (pconcat ? a b).