Stream: Ltac2

Topic: Early typing of Ltac2 Notations?

view this post on Zulip Gaëtan Gilbert (Oct 06 2023 at 08:44):

Currently you can write ill-typed ltac2 notations which fail only when used, eg

Ltac2 Notation "bad" := (() ()).
Goal True.
bad. (* this expression has type unit and is not a function *)

I wonder if we could run typechecking on the body of the notation when it's declared.

Because of type inference limitations it would forbid using the bound variables polymorphically, ie

Ltac2 Notation "use_identity" identity(tactic) :=
  identity ();
  identity 1.

Ltac2 Eval use_identity (fun x => x).

would not work, but are such notations ever useful in practice?

AFAICT ltac2 notations are not used for their typing delay effect, they're only used for the grammar rule effect.

view this post on Zulip Gaëtan Gilbert (Oct 06 2023 at 08:47):

cc @Pierre-Marie Pédrot

Last updated: Oct 12 2024 at 12:01 UTC