Matita HomeMatita Homedefault "s" u1 … un
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 u1 … un are the URIs of the definitions and theorems of the cluster. The number 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 x | a theorem of type ∀A.∀x,y:A.eq A x y → eq A y x | a 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 arguments | ||||||||||
| false | an inductive type of type Prop without constructors | ||||||||||
| absurd | a theorem of type ∀A:Prop.∀B:Prop.A → Not A → B |