X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter4.ma;h=fd0f711443a8554f57061c1d22c4b39463a540e9;hb=7aa41e02e64bd09df253cc4267a44b4f49b16e03;hp=76065b6dbac07ba30ade03af9332d108d71cb997;hpb=cd1ea2cc540bf000db797a497314028ce0fda0fa;p=helm.git

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).