The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

According to Leo's talk at the recent CPP workshop, lean does not use Z3 
itself, to avoid awkward encodings of type theory in FOL.  However, he says 
that almost all of the techniques used in Z3 can be adapted fairly readily to 
type theory, so most of Z3 will be in some sense built in.  

        - B

> On Feb 25, 2016, at 03:37, Soegtrop, Michael 
> <michael.soegtrop AT intel.com>
>  wrote:
> 
> Dear Saulo,
> 
> since they are looking into automation, I wonder if they plan to use Z3 for 
> some of its backend work. The manual doesn't mention Z3 ...
> 
> Otherwise the choice between Lean and Coq looks like the choice between F# 
> and OCaml.
> 
> Best regards,
> 
> Michael
> 
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928