From: matitaweb Date: Sat, 5 Nov 2011 16:56:56 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~2134 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e304931d5cb935c91402a5160c2150aeca0ea2b;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 5da976a52..b21fd3e17 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -149,7 +149,8 @@ inductive opp : a href="cic:/matita/tutorial/chapter1/bank.ind(1,0,0)"bank/a (* In precisely the same way as "bank" is the smallest type containing east and west, opp is the smallest predicate containing the two sub-cases east_west and weast_east. If you have some familiarity with Prolog, you may look at opp as the -predicate definined by the two clauses - in this case, the two facts - +predicate defined by the two clauses - in this case, the two facts - ast_west and +west_east. Between opp and opposite we have the following relation: opp a b iff a = opposite b