Tactic sequence partition function #273

New issue

Open

opened 2025-08-11 11:55:58 -07:00 by aniva · 0 comments

aniva commented

2025-08-11 11:55:58 -07:00

Owner

We need a function that can take a tactic sequence and partition it into individual tactics.

This is related to Project No. 3

e.g.

Input:

intro x; apply x
cases h

would become

intro x
apply x
cases h

For nested tactics such as branches in cases, we don't need to handle them.

We need a function that can take a tactic sequence and partition it into individual tactics. This is related to Project No. 3 e.g. Input: ```lean intro x; apply x cases h ``` would become ``` intro x apply x cases h ``` For nested tactics such as branches in `cases`, we don't need to handle them.