Stream: Ltac2

Topic: Ltac2 in Notations


view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Dec 16 2021 at 18:56):

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

view this post on Zulip Gregory Malecha (Dec 16 2021 at 18:57):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gregory Malecha (Dec 16 2021 at 19:01):

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

view this post on Zulip Notification Bot (Dec 16 2021 at 19:20):

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


Last updated: Jan 31 2023 at 10:01 UTC