Stream: Ltac2

Topic: ✔ matches_subterm

Patrick Nicodemus (Oct 19 2022 at 11:08):

(deleted)

Patrick Nicodemus (Oct 19 2022 at 11:11):

(deleted)

Patrick Nicodemus (Oct 19 2022 at 11:11):

(deleted)

Patrick Nicodemus (Oct 19 2022 at 11:11):

(deleted)

Notification Bot (Oct 19 2022 at 11:21):

Patrick Nicodemus has marked this topic as resolved.

Gaëtan Gilbert (Oct 19 2022 at 11:23):

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 *)

Patrick Nicodemus (Oct 19 2022 at 11:27):

Thank you!

Patrick Nicodemus (Oct 19 2022 at 11:29):

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

Gaëtan Gilbert (Oct 19 2022 at 11:35):

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)))

Patrick Nicodemus (Oct 19 2022 at 11:36):

Are there special properties to the exception raised by zero other than what is spelled out on the Ltac2 docs page?

Patrick Nicodemus (Oct 19 2022 at 12:14):

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: Oct 13 2024 at 01:02 UTC