Stream: Coq devs & plugin devs

Topic: Ltac2 FFI : building types and constructors


view this post on Zulip Mathis Bouverot-Dupuis (Jul 11 2024 at 13:53):

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.

view this post on Zulip Gaëtan Gilbert (Jul 11 2024 at 14:01):

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