Stream: Coq users

Topic: Ltac1 reference:()

Janno (Oct 04 2023 at 16:59):

I see that Ltac1 notation can use the reference(..) argument type and also that there's a reference:(..) quotation but I am not sure how to make use of references in Ltac1. Is there a way to go from a reference to a term? Do any tactics accept references?

Gaëtan Gilbert (Oct 04 2023 at 17:21):

there's the reduction delta lists

Goal 2 + 2 = 4.
let p := reference:(plus) in
cbv [p].

Janno (Oct 04 2023 at 17:29):

I see. I was trying unfold but that doesn't seem to work. EDIT: it does actually work. I was just using an invalid reference :face_palm:

Janno (Oct 04 2023 at 17:29):

And I guess there is no way to get a fresh constant out of a reference, is there?

Gaëtan Gilbert (Oct 04 2023 at 17:31):

probably not

Last updated: Oct 13 2024 at 01:02 UTC