From 60610b9013095e8e3f060ad3ab24e62902757d91 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 16 Nov 2011 12:45:15 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 2 ++ 1 file changed, 2 insertions(+) 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). -- 2.39.2