[Easycrypt-club] Hammers

Bas Spitters b.a.w.spitters at gmail.com
Wed Jan 24 15:33:56 CET 2018

There has been a lot of work on "hammers" for various systems.
E.g. HOL(y)hammer.

They return the information they get from the SMT solver so that they
can be stored in the proof scripts. This saves a lot of recomputation
Is this feasible for EC too?

More information about the Easycrypt-club mailing list