Stream: Coq users

Topic: Beginner : iterator on a context in Ltac

Louise Dubois de Prisque (Jan 22 2021 at 12:27):

Hello everyone,

I am sorry if my question is trivial, but how and is it possible to write a tactic which allows to iter on all hypothesis in the context, and apply a certain function (constr or ltac on it). I struggle with the 'match context' I think.

Guillaume Melquiond (Jan 22 2021 at 12:42):

Put your action next to change, then you can do repeat foo.

Ltac foo :=
  match goal with
  | H: ?P |- _ =>
    lazymatch P with
    | id _ => fail
    | _ => change P with (id P) in H
    end
  end.

Louise Dubois de Prisque (Jan 28 2021 at 16:00):

Thank you for your help !

Last updated: Oct 03 2023 at 19:01 UTC