I'm trying to use Ltac2 in notations but I keep running into issues with implicit parameters. Here's a small example:

```
Variant Y (t : Type) : Type := ANY.
Arguments ANY {_}.
Definition BAR (x : Y nat) : nat := 1.
Notation "'MAKE_IT' x" :=
(ltac2:(refine constr:(BAR ltac2:(refine (Constr.pretype x)))))
(at level 0, x at next level).
Definition t : nat :=
MAKE_IT ANY.
```

This fails with the error:

```
Error: Cannot infer the implicit parameter t of ANY whose type is "Type"
```

Is there any way to get something like this to work? In particular, the context of the notation argument is used to determine the type of the argument. The Ltac2 documentation suggests that the `pretype`

function uses the information from the current goal.

it uses the environment of the goal, but doesn't use the expected type

I see. Is there any way to massage the above tactics to work?

I should be more specific. I need to compute some values in Ltac/Ltac2 and then construct a term that mentions that argument to the notation.

something like

```
Ltac2 pretype_for_goal c := pretype (mkCast (c,goal())
```

then use that instead of pretype?

apparently ltac2 api doesn't have a sane way to build casts since the `cast`

type is abstract x_x

it seems like you can use the Unsafe module to build a `kind`

, but you can only do that for `constr`

, not `preterm`

but i guess i can write an Ltac2 primitive...

This topic was moved here from #Coq users > Ltac2 in Notations by Karl Palmskog

Last updated: May 31 2023 at 03:30 UTC