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