Stream: Coq users

Topic: trouble using autosubst2


view this post on Zulip Cody Roux (Feb 16 2022 at 16:21):

Does anyone around here have experience using autosubst-2?

I'm having a bit of trouble even using the notation t[theta], which may be related to a warning I'm getting:

Warning: Notation "_ [ _ ]" was already used in scope subst_scope.
[notation-overridden,parsing]

Any thoughts?

view this post on Zulip Cody Roux (Feb 16 2022 at 16:21):

(ping @Yannick Forster )

view this post on Zulip Yannick Forster (Feb 16 2022 at 16:24):

Did you generate the code using the Haskell implementation of Autosubst 2?

view this post on Zulip Cody Roux (Feb 16 2022 at 16:29):

Yep! It works like a peach!

view this post on Zulip Cody Roux (Feb 16 2022 at 16:30):

I can paste the sig file if you like...

view this post on Zulip Cody Roux (Feb 16 2022 at 16:30):

or the generated file

view this post on Zulip Yannick Forster (Feb 16 2022 at 16:32):

can you send me both? :)

view this post on Zulip Cody Roux (Feb 16 2022 at 17:13):

Sent!

view this post on Zulip Cody Roux (Feb 16 2022 at 18:33):

FYI, Yannick kindly helped me figure out the issue: it was a few lines of the generated code that needed to be commented out.


Last updated: Feb 06 2023 at 12:04 UTC