What do names like
This topic was moved here from #Coq Platform devs & users > cClosure functions by Karl Palmskog.
this seems to be a question about
kernel/cClosure.ml, so unrelated to the Platform.
Thanks, this is definitely the channel I thought I was in.
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
knr is "result" (the
knh is probably "head"), and I'm guessing
n is "neutral" or "normal". The
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