Thanks for sharing! I suggest the following article:
ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop You may want to try the 'implicit' theorem-proving style and also use Z3 as your external constraint-solver. Doing so should cut down the need for writing a lot of theorem-proving code. On Saturday, August 19, 2017 at 1:32:21 AM UTC-4, Fujii Ken-ichi wrote: > > I am building embedded drivers for RX110 series. > It is still on the way, but since the bit manipulation functions for that > has been completed, it will be released. > > https://github.com/fujiik102/ats-rx-drivers > > Bit.sats in the above describes bit manipulation functions and the > definitions necessary for them. > Bit.dats and BitInt.hats describe the implementation of the > implementations and propositions of the functions (BitInt.hats is included > from Bit.dats). > > Pin.sats and Pin.dats are defining and implementing general-purpose I / O > drivers for pins, but they are still in the middle. > > > Use it as you like. > > -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/f1ca83bc-1e9d-460b-af6b-f535985c4748%40googlegroups.com.
