Gregory Malecha (Aug 27 2022 at 14:06): Gregory Malecha (Aug 27 2022 at 14:06):What do names like knr, knit, kni mean?
Notification Bot (Aug 27 2022 at 16:08):This topic was moved here from #Coq Platform devs & users > cClosure functions by Karl Palmskog.
Karl Palmskog (Aug 27 2022 at 16:08):this seems to be a question about kernel/cClosure.ml, so unrelated to the Platform.
Gregory Malecha (Aug 28 2022 at 01:13):Thanks, this is definitely the channel I thought I was in.
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: May 28 2023 at 13:30 UTC