Stream: quantum computing

Topic: basics


view this post on Zulip Anthony Bordg (Jul 04 2019 at 12:05):

@Hanna Lachnitt @Yijun He What about a theory Basics.thy to collect very basic things like set_two, set_fourand so on which are duplicated across various files in the library ?
Of course, it's useful only if the attribute [simp] still works properly.

view this post on Zulip Anthony Bordg (Jul 04 2019 at 22:08):

Done!
I factored out various very basic results into a single theory named Basicswith a rough classification of these results. Thanks to that I cleaned the other theories (no modification was needed, the attributes [simp] work just fine, I only removed the trivial results). There is no duplication anymore.
So, in the future please use this theory.

view this post on Zulip Anthony Bordg (Oct 14 2019 at 12:05):

When starting a new theory, I advice to import Basics so that Sledgehammer can search it and use the very basic results proved therein.


Last updated: Aug 15 2022 at 02:13 UTC