Patrick Nicodemus has marked this topic as resolved.
Require Import Ltac2.Ltac2. Ltac2 rec all_successes_rec e f := match Control.case (fun () => f e) with | Err _ =>  | Val v => let (v, k) := v in v :: all_successes_rec e k end. Ltac2 all_successes e f := match Control.case f with | Err _ =>  | Val v => let (v, k) := v in v :: all_successes_rec e k end. Goal forall (a b c d : nat), a + b + c + d = 5. Proof. intros a b c d. Ltac2 Eval all_successes Not_found (fun () => Pattern.matches_subterm pat:(?z + _) constr:(a + b + c + d)). (* match for z=a+b+c, match for z=a+b, match for z=a *)
It was the "Not_found" thing I was having trouble with, I was not sure if the behavior of the "linked list" would depend on the choice of exception fed into the second input of case
In this case I don't think it does
tbh I think it's pretty rare for the exception to change semantics, at most they tend to be used to produce the final error (ie some tactics look like
foo + (fun e => bar + (fun e' => zero e)))
Are there special properties to the exception raised by
zero other than what is spelled out on the Ltac2 docs page?
Also if I am trying to make state changes to the proof in each iteration of the loop, are these all going to get undone?
Last updated: Jun 10 2023 at 06:31 UTC