Matita Home

`default "s" u`

_{1} … u_{n}

- Synopsis:
- Action:
It registers a cluster of related definitions and theorems to be used by tactics and the rendering engine. Some functionalities of Matita are not available when some clusters have not been registered. Overloading a cluster registration is possible: the last registration will be the default one, but the previous ones are still in effect.

**s**is an identifier of the cluster and**u**are the URIs of the definitions and theorems of the cluster. The number_{1}… u_{n}**n**of required URIs depends on the cluster. The following clusters are supported.**Table 9.1. clusters**name expected object for 1st URI expected object for 2nd URI expected object for 3rd URI expected object for 4th URI expected object for 5th URI expected object for 6th URI expected object for 7th URI expected object for 8th URI expected object for 9th URI expected object for 10th URI expected object for 11th URI equality an inductive type (say, of type **eq**) of type ∀A:Type.A**→****Prop**with one family parameter and one constructor of type ∀x:A.eq A xa theorem of type **∀**A.**∀**x,y:A.eq A x y**→**eq A y xa theorem of type **∀**A.**∀**x,y,z:A.eq A x y**→**eq A y z**→**eq A x z**∀**A.**∀**a.**∀**P:A**→****Prop**.P x**→****∀**y.eq A x y**→**P y**∀**A.**∀**a.**∀**P:A**→****Prop**.P x**→****∀**y.eq A y x**→**P y**∀**A.**∀**a.**∀**P:A**→****Set**.P x**→****∀**y.eq A x y**→**P y**∀**A.**∀**a.**∀**P:A**→****Set**.P x**→****∀**y.eq A y x**→**P y**∀**A.**∀**a.**∀**P:A**→****Type**.P x**→****∀**y.eq A x y**→**P y**∀**A.**∀**a.**∀**P:A**→****Type**.P x**→****∀**y.eq A y x**→**P y**∀**A.**∀**B.**∀**f:A**→**B.**∀**x,y:A.eq A x y**→**eq B (f x) (f y)**∀**A.**∀**B.**∀**f:A**→**B.**∀**x,y:A.eq A x y**→**eq B (f y) (f x)true an inductive type of type **Prop**with only one constructor that has no argumentsfalse an inductive type of type **Prop**without constructorsabsurd a theorem of type **∀**A:Prop.**∀**B:Prop.A**→**Not A**→**B