Когда я импортирую файлы теории, которые имеют определенные константы (для рекурсивных функций или определений), например f
, как я могу скрыть такую константу в текущем файле теории? Другими словами, я хочу убедиться, что f
является свободной переменной. Я не хочу менять импортированные файлы.Как скрыть определенные константы
4
A
ответ
6
Это точно цель команды hide_const
. НАПРИМЕР,
hide_const f
будет полностью удалить определенную константу f
из текущего контекста (и, таким образом, сделать его недоступным). Если вы используете
hide_const (open) f
вместо этого, только базовое имя скрыто (т.е. f
), но квалифицированное имя (например, A.f
если f
была определена в теории A
) до сих пор работает.
Существуют аналогичные команды для классов, типов и фактов: hide_class
, hide_type
и hide_fact
. См. Также the Isabelle/Isar Reference Manual, стр. 105.