feat: automatic `try?` suggestions for empty `by`, unsolved goals, and `sorry`#13830

Draft

nomeata wants to merge 38 commits into

joachim/auto-try

Commits on May 20, 2026

feat: auto-`try?` via post-elab hook with `autoTry.{onEmptyBy,onUnsolvedGoal,onSorry}` options

nomeata
and
claude
committed
refactor(autoTry): drop sorry-term, skip multi-elab combinators, expand tests

nomeata
and
claude
committed
refactor(autoTry): replace hard-coded combinator list with uniqueness heuristics

nomeata
and
claude
committed
refactor(autoTry): replace `TriggerKind` magic numbers with a real inductive; drop redundant `private`s

nomeata
and
claude
committed
chore(autoTry): drop unnecessary `public` and `meta` qualifiers from imports

nomeata
and
claude
committed
refactor(autoTry): apply review cleanup batch

nomeata
and
claude
committed
refactor(try?): factor out suggestion-collection entry points

nomeata
and
claude
committed

Commits on May 21, 2026

Commits on May 25, 2026

Commits on May 26, 2026

fix(autoTry): scope the message walk to the current command and dedup

nomeata
and
claude
committed