Stream: Ltac2

Topic: ✔ matches_subterm


view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 11:08):

(deleted)

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 11:11):

(deleted)

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 11:11):

(deleted)

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 11:11):

(deleted)

view this post on Zulip Notification Bot (Oct 19 2022 at 11:21):

Patrick Nicodemus has marked this topic as resolved.

view this post on Zulip 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 *)

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 11:27):

Thank you!

view this post on Zulip 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

view this post on Zulip 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)))

view this post on Zulip 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?

view this post on Zulip 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: Jan 31 2023 at 11:01 UTC