Not really. It basically generates a number of type (in)equalities and outsources finding the solution to Microsoft Z3 theorem prover, which you cannot use for anything commercial.