commit by user andrea

[helm.git] / weblib / tutorial / chapter4.ma

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 76065b6dbac07ba30ade03af9332d108d71cb997..fd0f711443a8554f57061c1d22c4b39463a540e9 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -107,6 +107,8 @@ inductive pitem (S: \ 5a href="cic:/matita/tutorial/chapter4/Alpha.ind(1,0,0)"\ 6Alp
  
 definition pre ≝ λS.\ 5a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S \ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)" title="null"\ 6bool\ 5/a\ 6.
 
+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).