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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
From Ltac2 Require Import Init.
Ltac2 Type t := inductive.
Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "ind_equal".
(** Equality test. *)
Ltac2 Type data.
(** Type of data representing inductive blocks. *)
Ltac2 @ external data : t -> data := "coq-core.plugins.ltac2" "ind_data".
(** Get the mutual blocks corresponding to an inductive type in the current
environment. Panics if there is no such inductive. *)
Ltac2 @ external repr : data -> t := "coq-core.plugins.ltac2" "ind_repr".
(** Returns the inductive corresponding to the block. Inverse of [data]. *)
Ltac2 @ external index : t -> int := "coq-core.plugins.ltac2" "ind_index".
(** Returns the index of the inductive type inside its mutual block. Guaranteed
to range between [0] and [nblocks data - 1] where [data] was retrieved
using the above function. *)
Ltac2 @ external nblocks : data -> int := "coq-core.plugins.ltac2" "ind_nblocks".
(** Returns the number of inductive types appearing in a mutual block. *)
Ltac2 @ external nconstructors : data -> int := "coq-core.plugins.ltac2" "ind_nconstructors".
(** Returns the number of constructors appearing in the current block. *)
Ltac2 @ external get_block : data -> int -> data := "coq-core.plugins.ltac2" "ind_get_block".
(** Returns the block corresponding to the nth inductive type. Index must range
between [0] and [nblocks data - 1], otherwise the function panics. *)
Ltac2 @ external get_constructor : data -> int -> constructor := "coq-core.plugins.ltac2" "ind_get_constructor".
(** Returns the nth constructor of the inductive type. Index must range between
[0] and [nconstructors data - 1], otherwise the function panics. *)
Ltac2 @ external get_projections : data -> projection array option
:= "coq-core.plugins.ltac2" "ind_get_projections".
(** Returns the list of projections for a primitive record,
or [None] if the inductive is not a primitive record. *)
|
