feat(goal): Add unshielded tactic execution mode #219

aniva · 2025-06-24T15:06:17-07:00

aniva commented

2025-06-24 15:06:17 -07:00

This is an improvement of the automatic mode.

AFAIK no non-decomposable tactic acts on multiple goals at once. However, it is very possible this would change in the future.

Moreover, the feature of only serializing delta's have been deleted, because now it is not clear which goal is the "parent" of a goal. A single goal can have multiple parents.

feat(goal): Use Site to indicate the scope of effect of a tactic.
refactor(repl): Condense conv and calc into tactic, in favour of tactic mode switches. This aligns with Lean's syntax category system.
fix(tactic): Allow conv and non-conv goals to coexist
fix(tactic): Bring fragment tactics in line with C/R paradigm. In particular, the sentinels of a conversion tactic mode goal is responsible for resuming the parent when it exits.

This is an improvement of the automatic mode. AFAIK no non-decomposable tactic acts on multiple goals at once. However, it is very possible this would change in the future. Moreover, the feature of only serializing delta's have been deleted, because now it is not clear which goal is the "parent" of a goal. A single goal can have multiple parents. - feat(goal): Use `Site` to indicate the scope of effect of a tactic. - refactor(repl): Condense conv and calc into tactic, in favour of tactic mode switches. This aligns with Lean's syntax category system. - fix(tactic): Allow conv and non-conv goals to coexist - fix(tactic): Bring fragment tactics in line with C/R paradigm. In particular, the sentinels of a conversion tactic mode goal is responsible for resuming the parent when it exits.

aniva added this to the 0.4.0 milestone 2025-06-24 15:06:17 -07:00

aniva added the

category

feature

part/Goal

labels 2025-06-24 15:06:18 -07:00

aniva self-assigned this 2025-06-24 15:06:18 -07:00

aniva added 1 commit 2025-06-24 15:06:18 -07:00

8e35926b5c

feat(goal): Tactic action site

aniva added a new dependency 2025-06-25 10:46:48 -07:00

#188 Unshielded Tactic Execution