+(*
\ 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
]
qed.
-(* \ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
+(*
+\ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
There is still another possibility, however, namely to mix the program and its
specification into a single entity. The idea is to refine the output type of the
div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a
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