Я сделал grep в папке src/HOL с instance+[ ]nat
и instantiation+[ ]nat
, и, возможно, я нашел все классы классов, которые были созданы для nat
.Как показать, какие классы классов были созданы для nat, int и т. Д.?
Поскольку это важно, что я смотрю на то, как int
, rat
и real
создали экземпляр, было бы удобно, если бы там была команда для выполнения этого, как print_dependencies
, который будет показывать зависимости для класса типа.
Ниже я показываю все команды печати и визуализации, которые я нашел, просто просмотрев раскрывающийся список завершения команды при вводе print_
.
Я также показываю экземпляры для nat
, которые я нашел в файлах корневой папки src/HOL, где главы соответствуют документу HOL.
subsection {* Nat class instantiations *}
(*
Ch.15 Nat
zero
comm_monoid_diff
comm_semiring_1_cancel
linorder
order_bot
no_top
linordered_semidom
no_zero_divisors
wellorder proof
ordered_cancel_comm_monoid_diff
distrib_lattice
Ch.37 Int
Ch.39 Divides
semiring_numeral_div
Ch.42 Semiring_Normalization
comm_semiring_1_cancel_crossproduct
Ch.72 Fact
fact
Ch.73 Parity
even_odd
Ch.74 GCD
gcd
Gcd
*)
Визуализация и печать команды:
subsection{*Visualize and Print*}
class_deps (*
locale_deps *)
thm_deps allI conjI
code_deps If
(*--PRINTS-----*)
print_locale ab_semigroup_add
print_facts
print_statement plus_nat_def times_nat_def
print_attributes
print_abbrevs
print_binds
print_context
print_state
print_coercions
print_commands
print_defn_rules
print_locales
print_methods (*
print_rules *)
print_antiquotations (*
print_ast_translation *)
print_bnfs
print_bundles
print_case_translations
print_cases (*
print_claset *)
print_classes
print_codeproc (*
print_codesetup *)
print_dependencies ab_semigroup_add(*
print_induct_rules *)
print_inductives
print_interps ab_semigroup_add
print_options
print_orders
print_quot_maps
print_quotconsts
print_quotients
print_quotientsQ3
print_quotmapsQ3 (*
print_simpset *)
print_syntax
print_theorems! (*
print_theory! *)
print_trans_rules (*
print_translation *)
Спасибо. Определенно, как просили. Я еще не могу голосовать, или я проголосую. –
Панель вывода Isabelle/jEdit еще не имеет собственного средства поиска, но jEdit делает. Поэтому, если вы просто скопируете текст в текстовый буфер и используете, например, гиперссылки на него, вы получаете больше удобства, чем командная строка grep старого стиля. – Makarius