From df544317f1496afa4ab356b0324d645a240d1dbf Mon Sep 17 00:00:00 2001 From: matitaweb Date: Wed, 7 Mar 2012 10:37:08 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 7260a33af..e3dfd1d44 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -231,7 +231,8 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)" ] qed. -(* h2 class="section"Mixing proofs and computations/h2 +(* +h2 class="section"Mixing proofs and computations/h2 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 -- 2.39.2