From 2e5d77caec4504b736af370743df2e460e9590f3 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 13 Mar 2012 15:12:07 +0000 Subject: [PATCH] manual correction to tutorial/chapter2.ma --- weblib/tutorial/chapter2.ma | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index e3dfd1d44..2942d6152 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -1,4 +1,6 @@ +(* h1 class="section"Induction and Recursion/h1 +*) include "basics/types.ma". (* Most of the types we have seen so far are enumerated types, composed by a @@ -282,4 +284,4 @@ example quotient7: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"wi example quotient8: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"witness/a … (a href="cic:/matita/tutorial/chapter2/div2Pagain.def(4)"div2Pagain/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a)))))) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a))), a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉. // qed. -prepre /pre/pre \ No newline at end of file +prepre /pre/pre -- 2.39.2