Ssreflect Users Discussion List

[Enrico Tassi <>]

On Fri, Feb 06, 2015 at 10:11:02AM -0800, Daniel Selsam wrote:
> Hi,
> 
> Thank you for responding so quickly. 
> 
> I am experimenting with machine-learning assisted automated theorem
> proving in Coq. Right now my system gets stuck on some simple lemmas
> from ssreflect that involve rewriting an instance of a pattern besides
> the first, because I have not been able to systematically enumerate a
> sufficient action space.

Ok, I'll look at the code and try to see if I can give you a decent API.

I think the most convenient way of printing all matches for me would be
to print the rewrite rule instance, that is pretty much the internal
data structure.

Would something like that work too?
  
  ((addnC n p), 1); ((addnC (n+p) n), 2); ...

Best,
-- 
Enrico Tassi