rocqnavi/glob_kind.mli at mca2html · affeldt-aist/rocqnavi · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
type kind =
  | Axiom (* Axiom, Parameter or Variable(s), Hypothes,es, Context outside any section *)
  | Definition
  | Coertion
  | Theorem
  | SubClass
  | CanonicalDeclaration
  | Example
  | Scheme
  | ClassDeclaration
  | ProjectionFromAStructure
  | Instance
  | ClassMethod
  | DefinitionalAssumption
  | LogicalAssumption
  | Primitive
  | SectionVariableReference (* Variable,s, Hypothes,es, Context *)
  | Inductive
  | InductiveVariant
  | Coinductive
  | Record
  | RecordVariant
  | CoinductiveRecord
  | Constructor
  | Notation
  | Binder
  | Require
  | ModuleReference (* Import, Module start / end *)
  | ModuleType
  | Other of string

type t = kind

val of_string : string -> kind
val to_string : kind -> string