Stream: Beginner Questions

Topic: How to import the HOL theory to use

view this post on Zulip Hongjian Jiang (Jul 26 2023 at 14:11):

I am looking for an efficient way to define the predicate, and I watch there exists a theory Predicate. So I import "HOL.Predicate" to include the datatype into my example. But I found that the final codes seem to hide these definition. 

hide_type (open) pred seq
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map the
  iterate_upto
hide_fact (open) null_def member_def

I don't think it is wise to rebuild these basic theories again. Is there any ideas to include these definition?

Thanks very much.

view this post on Zulip Mathias Fleury (Jul 26 2023 at 15:06):

Import Main, don't try to import HOL theories individually

view this post on Zulip Mathias Fleury (Jul 26 2023 at 15:07):

Predicate. at the start of each identiefier should do the job

view this post on Zulip Hongjian Jiang (Jul 26 2023 at 16:41):

I agree, thank you very much.

Last updated: Apr 28 2024 at 08:19 UTC