(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: Nsemigroup.v,v 1.6 2004/04/08 08:20:34 lcf Exp $ *) include "model/setoids/Nsetoid.ma". include "algebra/CSemiGroups.ma". (*#* **Example of a semi-group: $\langle$#⟨#[nat],[[+]]$\rangle$#⟩# *) (*#* Because addition is associative, the natural numbers form a CSemiGroup. *) inline procedural "cic:/CoRN/model/semigroups/Nsemigroup/nat_as_CSemiGroup.con" as definition.