Is there a way to check if given a variable name (as in an identifier), we can say if it corresponds to constant or a function within a coq plugin?

can you explain more?

As in:

```
Definition fooC1: nat := 3.
Definition fooF1: nat -> nat := id.
Definition fooF2: nat -> nat -> bool := Nat.eqb.
```

Here, `fooC`

is a constant (~~as in has kind ~~ but `*`

)`fooF1`

and `fooF2`

are functions.

I was hoping to find a way to distinguish between constants and functions.

What is a constant if not a constant function? ;)

Julio Di Egidio said:

What is a constant if not a constant function? ;)

Ah.. that's a good question..

Given a name, would it be possible to get hold of its type somehow?

```
Check fooC1.
```

or (with more details)

```
About fooC1.
```

No, I meant from a plugin.

I guess for that some AST fiddling is involved?

resolve a qualid with Nametab.locate

get the type with Environ.constant_type_in or combine Evd.fresh_global with the Retyping functions

Last updated: Oct 13 2024 at 01:02 UTC