Library MetaCoq.Template.BasicAst

Definition ident := string. Definition qualid := string. Definition kername := string.
Inductive name : Set :=
| nAnon
| nNamed (_ : ident).

Record inductive : Set := mkInd { inductive_mind : kername ;
inductive_ind : nat }.

Definition projection : Set := inductive × nat × nat .

Parametrized by term because term is not yet defined

Record def (term : Set) : Set := mkdef {
  dname : name;
  dtype : term;
  dbody : term;
  rarg : nat }.

Definition mfixpoint (term : Set) : Set :=
  list (def term).

The kind of a cast

Inductive cast_kind : Set :=
| VmCast
| NativeCast
| Cast
| RevertCast.

Inductive recursivity_kind :=
  | Finite
  | CoFinite
  | BiFinite .

Kernel declaration references global_reference

Inductive global_reference :=

| ConstRef : kername → global_reference
| IndRef : inductive → global_reference
| ConstructRef : inductive → nat → global_reference.