14.5 Commands

14.5 Commands

14.5.1 Class ident.

Declares the name ident as a new class.


Error messages:
  1. ident not declared
  2. ident is already a class
  3. Type of ident does not end with a sort


14.5.2 Class Local ident.

Declares the name ident as a new local class to the current section.

14.5.3 Coercion ident : ident1 >-> ident2.

Declares the name ident as a coercion between ident1 and ident2. The classes ident1 and ident2 are first declared if necessary.
Error messages:
  1. ident not declared
  2. ident is already a coercion
  3. FUNCLASS cannot be a source class
  4. SORTCLASS cannot be a source class
  5. Does not correspond to a coercion
    ident is not function.
  6. We do not find the source class ident1
  7. ident does not respect the inheritance uniform condition
  8. The target class does not correspond to ident2


When the coercion ident is added to the inheritance graph, non valid path coercions are ignored; they are signaled by a warning.
Warning :
  1. Ambiguous paths: [f11;..;fn11] : C1>->D1
      ...
      [f1m;..;fnmm] : Cm>->Dm


14.5.4 Coercion Local ident:ident1 >-> ident2.

Declares the name ident as a local coercion to the current section.

14.5.5 Identity Coercion ident:ident1 >-> ident2.

We check that ident1 is a constant with a value of the form [x1:T1]..[xn:Tn](ident2 t1..tm) where m is the number of parameters of ident2. Then we define an identity function with the type (x1:T1)..(xn:Tn)(y:(ident1 x1..xn)) (ident2 t1..tm), and we declare it as an identity coercion between ident1 and ident2.


Error messages:
  1. Clash with previous constant ident
  2. ident1 must be a transparent constant


14.5.6 Identity Coercion Local ident:ident1 >-> ident2.

Declares the name ident as a local identity coercion to the current section.

14.5.7 Print Classes.

Print the list of declared classes in the current context.

14.5.8 Print Coercions.

Print the list of declared coercions in the current context.

14.5.9 Print Graph.

Print the list of valid path coercions in the current context.

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.3.4.html at 8/10/98