]> matita.cs.unibo.it Git - helm.git/commitdiff
manual correction to tutorial/chapter2.ma
authormatitaweb <claudio.sacerdoticoen@unibo.it>
Tue, 13 Mar 2012 15:12:07 +0000 (15:12 +0000)
committermatitaweb <claudio.sacerdoticoen@unibo.it>
Tue, 13 Mar 2012 15:12:07 +0000 (15:12 +0000)
weblib/tutorial/chapter2.ma

index e3dfd1d4470a8bac423d9177f25e9b5b9d9ec49d..2942d61524b941cc00daa7c6e59adb49bf974416 100644 (file)
@@ -1,4 +1,6 @@
+(*
 \ 5h1 class="section"\ 6Induction and Recursion\ 5/h1\ 6
+*)
 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: \ 5a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"\ 6wi
 example quotient8: \ 5a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"\ 6witness\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/div2Pagain.def(4)"\ 6div2Pagain\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6)))))) 
        \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6))), \ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"\ 6ff\ 5/a\ 6〉.
 // qed. 
-\ 5pre\ 6\ 5pre\ 6 \ 5/pre\ 6\ 5/pre\ 6
\ No newline at end of file
+\ 5pre\ 6\ 5pre\ 6 \ 5/pre\ 6\ 5/pre\ 6