From 560dcf554215ac3b272555f68bf7536b49d72383 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 5 Jun 2006 11:38:24 +0000 Subject: [PATCH] bug fixed in doc --- matita/help/C/sec_terms.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index faa4f765f..6d359a7ac 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -344,7 +344,7 @@ [<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]… -[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…] +[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]… (co)inductive types declaration inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm' -- 2.39.2