Stream: Coq devs & plugin devs

Topic: cClosure functions


view this post on Zulip Gregory Malecha (Aug 27 2022 at 14:06):

What do names like knr, knit, kni mean?

view this post on Zulip Notification Bot (Aug 27 2022 at 16:08):

This topic was moved here from #Coq Platform devs & users > cClosure functions by Karl Palmskog.

view this post on Zulip Karl Palmskog (Aug 27 2022 at 16:08):

this seems to be a question about kernel/cClosure.ml, so unrelated to the Platform.

view this post on Zulip Gregory Malecha (Aug 28 2022 at 01:13):

Thanks, this is definitely the channel I thought I was in.

view this post on Zulip Jason Gross (Aug 28 2022 at 03:39):

They seem to have been introduced by @Bruno Barras in https://github.com/coq/coq/commit/bb7d7482724489521dde94a5b70af7864acfa802 with commit message " nouvelle implantation de la reduction
suppression de IsXtra du noyau"
I'm guessing based on "(* Computes a normal form from the result of knh. *)" that the r in knr is "result" (the h in knh is probably "head"), and I'm guessing n is "neutral" or "normal". The t in knit might be "term"?? Maybe k stands for "Krivine machine"? No idea about i (though really I'm just guessing for all of these.)


Last updated: Feb 01 2023 at 16:03 UTC