What is the type of `main0` function?

Question

What is the type of main0 function?

I'm writing gtk3 library. However the g_application_run() function needs argv. Of course, ATS language can use argv on main0 function. But what is the type?

Answer 1

The following code is declared in prelude/basics_dyn.dats:

//
symintr main0
//
fun
main_void_0
  ((*void*)): void = "ext#mainats_void_0"
fun
main_argc_argv_0
  {n:int | n >= 1}
  (argc: int n, argv: !argv(n)): void = "ext#mainats_argc_argv_0"
//
overload main0 with main_void_0
overload main0 with main_argc_argv_0
//

As you can see, main0 is overloaded with main_void_0 and main_argc_argv_0. The type argv(n) is essentially for a linear string array of size n that ends with the null value. Note that the null value is not counted as part of the size.