«С» означает «сертифицировано» (или «проверено»? Не уверен). Cterm - это термин, который прошел проверку. Антикатотация @{cterm …} позволяет вам просто записывать термины и напрямую получать cterm в различных контекстах (в этом случае, вероятно, в контексте ML, т.е. вы напрямую получаете значение cterm с предполагаемым содержимым). То же самое работает для обычных терминов, то есть @{term …}.
. Вы можете манипулировать cterms напрямую, используя функции из структуры Thm (которую, кстати, можно найти в ~~/src/Pure/thm.ML; большинство из этих основных MLфайлы находятся в каталоге Pure). Однако, по моему опыту, обычно проще просто преобразовать cterm в обычный термин (используя Thm.term_of - в отличие от Thm.cterm_of, это очень дешевая операция), а затем вместо этого работать с термином. Непосредственное манипулирование cterms действительно имеет смысл только в том случае, если вам нужен еще один cterm в конце, потому что повторная сертификация терминов довольно дорога (тем не менее, если ваш код вызывается очень часто, это, вероятно, не является проблемой производительности).
В большинстве случаев я бы сказал, что рабочий процесс выглядит так: если вы получаете cterm в качестве входных данных, вы превращаете его в обычный термин. Это вы можете легко проверить / разобрать / что угодно. В какой-то момент вам, возможно, придется снова превратить его в cterm (например, потому что вы хотите создать для него некоторую теорему или использовать ее каким-либо другим способом, связанным с ядром), а затем вы просто используете Thm.cterm_of для этого.
Я не знаю точно , что делает внутренняя антикатотация @{cterm …}, но я мог бы представить, что в конце дня он просто анализирует свой параметр как термин Изабель, а затем сертифицируетэто с текущим контекстом (то есть @{context}), используя что-то вроде Thm.cterm_of.