Stream: Ltac2

Topic: Ltac2 in Notations

Gregory Malecha (Dec 16 2021 at 18:53):

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.

Gaëtan Gilbert (Dec 16 2021 at 18:56):

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

Gregory Malecha (Dec 16 2021 at 18:57):

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

Gregory Malecha (Dec 16 2021 at 18:58):

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.

Gaëtan Gilbert (Dec 16 2021 at 18:58):

something like

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

then use that instead of pretype?

Gaëtan Gilbert (Dec 16 2021 at 18:59):

apparently ltac2 api doesn't have a sane way to build casts since the cast type is abstract x_x

Gregory Malecha (Dec 16 2021 at 19:00):

it seems like you can use the Unsafe module to build a kind, but you can only do that for constr, not preterm

Gregory Malecha (Dec 16 2021 at 19:01):

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

Notification Bot (Dec 16 2021 at 19:20):

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

Last updated: Sep 15 2024 at 13:02 UTC