From Ocaml I can use `Tac2interp.eval_global kn`

to build the Ltac2 `valexpr`

corresponding to an Ltac2 global constant `kn`

. Is there something equivalent to build the `valexpr`

corresponding to an Ltac2 type or to an Ltac2 constructor ?

More specifically I have an Ltac2 type similar to the following :

```
Ltac2 Type mytype := [ A | B ].
```

and I would like to construct the `valexpr`

corresponding to say `A`

.

ltac2 types are not values

the representation of algebraic types is `ValInt i`

for constant constructors and `ValBlk (i, args)`

for non-constant constructors such that

```
Ltac2 Type t := [ A (* ValInt 0 *)
| B (x, y) (* ValBlk (0, [|x;y|]) *)
| C (* ValInt 1 *)
| D (z) (* ValBlk (1, [|z|]) *) ].
```

Last updated: Oct 13 2024 at 01:02 UTC