How to construct non-trivial Lean objects from FFI?

Stream: lean4

[Akhil Reddimalla]

From the lean4 manual, (https://lean-lang.org/lean4/doc/dev/ffi.html) I have understood how to construct Inductive types that have no parameters(enums) and how to construct inductive types with a single case. How would I construct an object with any number of fields in multiple cases? If the specific case I want has no fields , then I can use lean_box, but if the case has fields what can I do?

[Mario Carneiro]

The simplest way to find out the answers to these kind of questions is to write a function that writes into such an inductive type or creates it or what have you and then compile it and look at the generated .c file to find out what lean did

[Mario Carneiro]

inductive Bla (α : Type)
  | zero : Bla α
  | one : Bla α
  | two : α → Bla α

def foo (a : α) : Bla α :=
  .two a

produces:

LEAN_EXPORT lean_object* l_foo___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}

[Akhil Reddimalla]

Thanks for the info. I will try this method