The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Hi,

Le 21/09/2013 18:25, t x a écrit :
> To check if I understand your logic correctly --
> 
> Suppose we defined "agressive_auto" =
>   // this is probably not really correct
>   repeat (
>     forall x in Hint Extern (sorted by precedence);
>       if we can apply x, apply x
>   )
> 
> Then basically, the property of "don't change state if it can't be proved" 
> can
> be simulated with:
> 
>   solve[ agressive_auto ];
> 
> and the property of never fail can be simulated with
> 
>   try( solve [ agressive_auto ] );
> 
> in which case, auto "sorta =" try (solve [agressive_auto]) ?

What you suggest would work only when there is only one possible path (or no
backtracking).

Best,
-- 
Cyril Cohen