Stream: Ltac2

Topic: Program mode with tactics in terms

view this post on Zulip David Swasey (Apr 09 2024 at 15:17):

I'd like to place an antiquotationltac2:(tac) in the RHS of a program mode definition #[program] Definition s.t. the tactic tac leaves unresolved evars to be solved as obligations.

This does not presently seem possible, and I wonder how big a change it would be (and what would be involved).

Contrived example:

Require Import Coq.Program.Tactics.
Require Import Ltac2.Ltac2.
Section test.
    Context (goal : nat -> Prop).

    Succeed #[program] Definition cats := goal _.

    Succeed Check ltac2:(
        let c := open_constr:(goal ?[n]) in
        eexact $c
    ).

    Fail #[program] Definition cats := ltac2:(
        let c := open_constr:(goal ?[n]) in
        eexact $c
    ).
End test.

Thanks,
-dave

view this post on Zulip Janno (Apr 09 2024 at 16:11):

I am still digging but it seems like named holes are forbidden from becoming obligations by the misleadingly named mark_obligation_evar function in pretyping.ml. (Its name is misleading because it only actually marks the evars in a few select cases and otherwise does nothing.)

    Fail #[program] Definition cats := goal ?[n]. (* no Ltac2 needed for failure *)

view this post on Zulip Pierre-Marie Pédrot (Apr 09 2024 at 16:30):

IIRC obligation evars are recognized using the infamous evar_kind marker, so this is definitely buggy territory.

Last updated: Oct 12 2024 at 13:01 UTC