Ltac2
1 program
Added 2026-03-12T10:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: Ltac 2
Provenance: commit cf0493da27 · authored 2026-03-12T23:47:47+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Reflexivity Tactic with Repeat
Provenance: commit cf0493da27 · authored 2026-03-12T23:47:47+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
From Ltac2 Require Import Ltac2.
(** A tactic that proves goals of the form [n = n] *)
Ltac2 solve_refl () :=
match! goal with
| [ |- ?x = ?x ] => reflexivity ()
| [ |- _ ] =>
Control.zero (Tactic_failure None)
end.
(** Repeatedly apply a tactic until it fails *)
Ltac2 rec repeat0 (t : unit -> unit) : unit :=
Control.plus (fun () => t (); repeat0 t) (fun _ => ()).
(** Solve universally quantified reflexivity goals *)
Ltac2 solve_forall_refl () :=
repeat0 (fun () => intro _);
solve_refl ().
Goal forall (n : nat), n = n.
Proof.
solve_forall_refl ().
Qed.
Goal forall (s : string), s = s.
Proof.
solve_forall_refl ().
Qed.