Stream: MetaCoq

Topic: Basics of MetaCoq - How to inline quote/unquote


view this post on Zulip William Hibbert (May 01 2024 at 05:17):

Hi. Firstly sorry If I am using this forum incorrectly, this is my first time using Zulip and I cant find any specific on-boarding information for this stream.
I'm currently self studying learning Coq and am branching out to learning MetaCoq. The only Tutorial I can find that seems readily accessible to me is the [TutorialFest@POPL'24] MetaCoq Tutorial on YouTube. That tutorial session seems to have a bundled in file MetaCoqPrelude which defines commands $quote and $unquote that allows one to inline quote and then unquote terms without say using MetaCoq Quote Definition and carrying around a bunch of definitions.

I can't figure out how to do this myself nor does google help me out either. I looked on the git page for the tutorial but there does not seem to be the MetaCoqPrelude.v file there either. The tutorial says to ask here for help, so I was wondering if there was anyone present here who could assist / produce the .v file?

view this post on Zulip Yannick Forster (May 01 2024 at 07:50):

Here you go: https://github.com/MetaCoq/tutorials/blob/main/popl24/exercises/MetaCoqPrelude.v

view this post on Zulip William Hibbert (May 01 2024 at 07:56):

Many Thanks!


Last updated: Jul 23 2024 at 21:01 UTC