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?
Ju-sh has marked this topic as resolved.
Ju-sh has marked this topic as unresolved.
Yes, the docs are outdated in this regard
Okay, thank you!
Ju-sh has marked this topic as resolved.
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