Stream: MetaCoq

Topic: ✔ Definition of kername


view this post on Zulip 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?

view this post on Zulip Notification Bot (Dec 30 2021 at 16:47):

Ju-sh has marked this topic as resolved.

view this post on Zulip Notification Bot (Dec 30 2021 at 16:47):

Ju-sh has marked this topic as unresolved.

view this post on Zulip Yannick Forster (Dec 30 2021 at 16:56):

Yes, the docs are outdated in this regard

view this post on Zulip Julin S (Dec 30 2021 at 16:58):

Okay, thank you!

view this post on Zulip Notification Bot (Dec 30 2021 at 16:58):

Ju-sh has marked this topic as resolved.

view this post on Zulip 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: Aug 11 2022 at 03:02 UTC