Julin S (Dec 30 2021 at 16:47): Julin S (Dec 30 2021 at 16:47):This page gives a definition for kername like
Definition kername := string.
But when I do it locally, it gives
Check kername.
(*
kername = modpath × ident
: Set
*)
On searching the metacoq repo, I found a definition for a kername that matches this in here.
Is the one saying that kername is same as string a different kername?
Or could it be that docs wasn't updated since version is still beta?
Notification Bot (Dec 30 2021 at 16:47):Ju-sh has marked this topic as resolved.
Notification Bot (Dec 30 2021 at 16:47):Ju-sh has marked this topic as unresolved.
Yannick Forster (Dec 30 2021 at 16:56):Yes, the docs are outdated in this regard
Julin S (Dec 30 2021 at 16:58):Okay, thank you!
Notification Bot (Dec 30 2021 at 16:58):Ju-sh has marked this topic as resolved.
Julin S (Dec 30 2021 at 17:00):Is there any other docs for getting familiar with template-coq? Or would the source itself be the best place to look at? (for metacoq1.0~beta1+8.12).
Last updated: Jun 01 2023 at 13:01 UTC