From 1e304931d5cb935c91402a5160c2150aeca0ea2b Mon Sep 17 00:00:00 2001 From: matitaweb Date: Sat, 5 Nov 2011 16:56:56 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter1.ma | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2