On Fri, Jan 5, 2018 at 11:07 AM, cmp xchg <c0mpx...@gmail.com> wrote:
>
> example:
>
> fun {m,n:bv32} bvadd ( a:bv32(m), b:bv32(n) ) : bv32(bvadd(m,n))IIRC, William Blair did some work on an experimental prelude that used bv32 with the original work on using Z3 as an external solver. You can see some of it in 'contrib': https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/libats-/wdblair/prelude/SATS/integer.sats I'm not sure if the current Z3 solver work exposes bv32, etc. -- http://bluishcoder.co.nz -- 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/CALn1vHGmudbZ8%2Bu5tfWFZFmzXKy3fpeRNw1a2jphpr6BzsCQ3A%40mail.gmail.com.
