Is there a way to print the type of a term in ltac2 similar to how About does, where it shows which binders are implicit? The reason I'm not just using About, is because About only works for definitions, but I'd like this to work with partially applied functions.

I found how to get the type of a term using `type`

in ltac2. This snippet shows that along with how ltac2 and About show different types for `nth`

.

```
From Coq Require Import List.
From Ltac2 Require Import Ltac2.
From Ltac2 Require Import Constr.
From Ltac2 Require Import Printf.
About nth.
Ltac2 Eval
printf "";
printf "nth type according to ltac2: %t" (type open_constr:(nth)).
```

Output:

```
nth : forall [A : Type], nat -> list A -> A -> A
nth is not universe polymorphic
Arguments nth [A]%type_scope n%nat_scope l%list_scope default
nth is transparent
Expands to: Constant Coq.Lists.List.nth
nth type according to ltac2: (forall A : Type, nat -> list A -> A -> A)
- : unit = ()
```

I think implicit arguments can only be set for definitions... so `About`

would show that information, since it can only be given definitions.

The Ltac2 `type`

function takes any kind of term, so it will not do anything special for definitions. It functions more like `Check`

.

So I don't think this is directly possible. What is your end goal here?

I'm making a mod for a Minecraft-like video game. The player gets items in game that hold Coq terms. They can combine them together using application to get a new term. The mod calls into Coq to get the type information for the new term so that it can be displayed in game.

I'd like some kind of consistent output that works for both definitions and expressions, to make the mod easier to understand. Ltac2 and Check are showing the maximally implicit arguments with existentials, which are honestly easier to understand than than the `forall`

that About prints. However, the Ltac2 I currently have and the Check command are converting the non-maximal implicit arguments into regular arguments, which is confusing unless you know a lot about Coq already.

implicits are a property of references not terms

I don't think Ltac2 is the right kind of language for this type of query / interaction. @Kyle Stemen depending on the language your mod is implemented in, you should rather use something like serapi or directly the (unstable) OCaml API of Coq

As far as I can see this Elpi API does what you want.

```
% [coq.arguments.implicit GR Imps] reads the implicit arguments declarations
% associated to a global reference. See also the [] and {} flags for the
% Arguments command.
```

I took at look at Serapi. It says its in maintenance mode and replaced by coq-lsp, but the query interface for coq-lsp has even worse documentaiton.

Serapi seems to do about what the coqtop protocol can do, but with a more documented interface. I cannot find a way to get Serapi to print the type of an arbitrary expression, aside from asking Serapi to just run the Check command. When Serapi just runs the Check command, the only benefit it has over running Check through coqc is that it breaks up the pretty printed string into pieces.

Serapi has an option to query a definition, but it just shows the AST of the definition. It doesn't even show the type of the definition.

```
rlwrap sertop --printer=human
(Add () "Definition x:= 0. Definition y:= x.")
(Exec 3)
(Query () (Definition y))
> (Answer 3 Ack)
> (Answer 3
> (ObjList
> ((CoqConstr
> (Const
> ((Constant (KerName (MPfile (DirPath ((Id SerTop)))) (Id x)) ())
> (Instance (() ()))))))))
> (Answer 3 Completed)
```

One disadvantage to Elpi is that it doesn't come bundled with distro Coq installations. So the directions for my mod would have to explain how to install Coq along with Elpi.

I didn't try it, but I think the function that Michael linked to in Elpi is just the equivalent of the `About`

Vernac command, meaning that it will work when given a definition reference, but not when given a partially applied expression. For example, let's say I have the following definition:

```
Definition two_implicits [A: Type] (a: A) [B: Type] (b: B) : nat := 0.
```

I want to query how many additional arguments should be appended to the expression `two_implicits 0`

to fully apply the function. `Check (two_implicits 0)`

implies that it needs 2 more arguments. However, really it just needs 1 more argument: `(two_implicits 0 1)`

.

It might be solvable in ltac2 by taking `(two_implicits 0)`

as preterm, then repeatedly adding `_`

to the end until it stops type checking. Then it could repeatedly match on the resulting constr, and find which terms have the same name as the evars from the wildcards it added. The remaining terms that don't match its evars would have come from implicit variables. At that point it would need to print all of that information in some format.

However, that's pretty complex. So maybe Pierre-Marie is right that I should just directly call Coq APIs from Ocaml.

It might be solvable in ltac2 by taking (two_implicits 0) as preterm, then repeatedly adding _ to the end until it stops type checking

preterms already have implicits inserted so that won't work

preterms already have implicits inserted so that won't work

You're right, thank you. I was misinterpreting the output from my Coq script.

Last updated: Oct 12 2024 at 11:01 UTC