Enable handling of m-Coupled goals #20

aniva · 2023-10-07T16:11:54-07:00

aniva commented

2023-10-07 16:11:54 -07:00

Enable companion generation; Goals can now depend on each other (#18)
Enable hole filling via proof terms
Enable hole result collection. i.e. after a hole is filled its expression can be extracted

Files renamed:

Commands.lean -> Protocol.lean
Symbols.lean -> Symbol.lean

Refactoring:

Separated serialization logic from Goal.lean
Use goal states instead of goals

1. Enable companion generation; Goals can now depend on each other (#18) 2. Enable hole filling via proof terms 3. Enable hole result collection. i.e. after a hole is filled its expression can be extracted Files renamed: * `Commands.lean` -> `Protocol.lean` * `Symbols.lean` -> `Symbol.lean` Refactoring: * Separated serialization logic from `Goal.lean` * Use goal states instead of goals

aniva added the

category

feature

part/Goal

labels 2023-10-07 16:11:54 -07:00

aniva added 1 commit 2023-10-07 16:11:54 -07:00

42133f9b74

Add holes test stub

Move tests into their own namespaces

aniva added the

priority

medium

label 2023-10-07 16:12:49 -07:00

aniva added 2 commits 2023-10-15 17:17:54 -07:00

8c93d30ab7

Rename tactic to goal and restructure

9447d29e37

Store states instead of goals

1. Rename {Commands, Protocol}, and {Symbols, Symbol}
2. Store the root mvarId in the proof state along with goal indices
3. Add diagnostics function which prints out the state
4. Bump version to 0.2.6 (breaking change)

Documentations pending

aniva changed title from ~~Enable companion generation~~ to Enable handling of m-Coupled goals

2023-10-25 14:34:43 -07:00

aniva added 1 commit 2023-10-25 16:04:09 -07:00

0a0f0304a8

feat: Add proof continue and root extraction

aniva commented

2023-10-25 16:05:04 -07:00

Pending test on this case:

Σ' p: Prop, p

Also we need to expose an interface for (2) so the user doesn't have to rely on reduce

Pending test on this case: ```lean Σ' p: Prop, p ``` Also we need to expose an interface for (2) so the user doesn't have to rely on `reduce`

aniva added this to the 0.2.6 milestone 2023-10-25 16:05:23 -07:00

aniva added 1 commit 2023-10-25 22:20:31 -07:00

0ecfa9fc26

feat: Display user name in Goal structure

1. Modify `serialize_expression_ast` so its no longer a monad
2. Test existence of root expression

aniva added 1 commit 2023-10-26 11:22:31 -07:00

4ffd226cac

test: m-coupled goals

aniva added 1 commit 2023-10-26 22:48:37 -07:00

e98fb77f33

refactor: Separate goal printing and processing

Added a test for delta proof variables

aniva added 2 commits 2023-10-27 15:33:28 -07:00

b381d89ff9

feat: Assigning a goal with an expression

82f5494718

feat: Add REPL command for assigning an expression

aniva added 1 commit 2023-10-27 15:33:59 -07:00

ca7a081cac

Merge branch 'dev' into goal/dependency

aniva added 1 commit 2023-10-27 15:41:27 -07:00

427d819349

feat: Add REPL function for root expression

aniva merged commit c19fd1bcfb into dev

2023-10-27 19:30:21 -07:00

aniva deleted branch goal/dependency

2023-10-27 19:30:21 -07:00

aniva referenced this issue from a commit

2023-10-27 19:30:22 -07:00

Merge pull request 'Enable handling of m-Coupled goals' (#20) from goal/dependency into dev

aniva referenced this pull request

2023-10-28 16:38:06 -07:00

Companion Generation #18

aniva referenced this issue from a commit

2024-04-11 15:44:02 -07:00

Merge pull request 'Enable handling of m-Coupled goals' (#20) from goal/dependency into dev

Sign in to join this conversation.

No reviewers

No Label

No Milestone

No project

No Assignees

1 Participants

Notifications

Due Date

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

No due date set.

Dependencies

No dependencies set.

Reference: aniva/Pantograph#20