Unshielded Tactic Execution #188

New Issue

Closed

opened 2025-04-12 00:16:37 -07:00 by aniva · 2 comments

aniva commented 2025-04-12 00:16:37 -07:00

Owner

Copy Link

It would be a good idea to allow people to run simp_all and other tactics that act on multiple goals at once. Eventually SMT will require such a feature.

It would be a good idea to allow people to run `simp_all` and other tactics that act on multiple goals at once. Eventually SMT will require such a feature.

aniva added the

part/Goal

category

feature

labels 2025-04-12 00:16:37 -07:00

aniva self-assigned this 2025-04-12 00:16:37 -07:00

aniva added this to the 0.4.0 milestone 2025-04-14 16:48:50 -07:00

aniva changed title from Unshielded Tactic to Unshielded Tactic Execution 2025-06-20 12:42:11 -07:00

aniva modified the milestone from 0.4.0 to 0.3.3 2025-06-22 22:41:48 -07:00

aniva commented 2025-06-23 09:09:37 -07:00

Author

Owner

Copy Link

The goal for this is a rudimentary form of articulation. If the user executes a series of tactics at goal location 0, then they can string the tactics together to form a proof. It's not a perfect system.

The goal for this is a rudimentary form of articulation. If the user executes a series of tactics at goal location 0, then they can string the tactics together to form a proof. It's not a perfect system.

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

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

aniva commented 2025-06-26 15:58:34 -07:00

Author

Owner

Copy Link

Solved #219

Solved #219

aniva closed this issue 2025-06-26 15:58:34 -07:00

Sign in to join this conversation.

No Branch/Tag Specified

Branches Tags

dev

fix/calc-erase-goal

repl/test

main

v0.3.3

v0.3.2

v0.3.1

v0.3.0

v0.2.25

v0.2.24

v0.2.23

v0.2.22

v0.2.21

v0.2.20

v0.2.19

v0.2.19-alpha

v0.2.18

v0.2.14

v0.2.13

v0.2.12

v0.2.11

v0.2.10

v0.2.10-alpha

v0.2.9

v0.2.8

v0.2.7

v0.2.6

v0.2.5

0.2.3

0.1

Labels

Clear labels   

category

bug

Bugs, Test failures, Build failures

  

category

chore

Code cleanup

  

category

doc

Documentation

  

category

feature

New features and enhancements

  

category

optimization

Performance improvements

  

category

organization

Versioning and structure

  

part/Delation

Kernel to search view

  

part/Elab

Parsing and elaboration

  

part/Environment

Environments, Library, Catalog

  

part/FFI

Library and FFI

  

part/Frontend

Driving the Lean compiler

  

part/Goal

Goal evolution, proof terms, tactics

  

part/REPL

For text based interaction

  

part/Serial

Serialization, IO

  

priority

high

  

priority

irrelevant

Issues that will not be fixed or are intended features

  

priority

low

For things that don't impede release schedule

  

priority

medium

  

priority

pending-measurement

For nebulous problems

No Label

category

bug

category

chore

category

doc

category

feature

category

optimization

category

organization

part/Delation

part/Elab

part/Environment

part/FFI

part/Frontend

part/Goal

part/REPL

part/Serial

priority

high

priority

irrelevant

priority

low

priority

medium

priority

pending-measurement

Milestone

Clear milestone

No items

No Milestone

0.3.3

Projects

Clear projects

No project

Assignees

Clear assignees

No Assignees

aniva

1 Participants

Notifications

Subscribe

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Depends on

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

aniva/Pantograph

Reference: aniva/Pantograph#188

No description provided.