feat: Condensed interface #85

Merged

aniva merged 27 commits from serial/expr into dev 2024-08-15 22:41:59 -07:00

Conversation 0 Commits 27 Files changed 13 +241 -124

aniva commented 2024-06-26 06:34:26 -07:00

Owner

Copy link

This replaces the sexp based interface for emitting structures.

To facilitate this, the user has to execute MetaM monads. The state of this monad can be queried from any individual goal by GoalState.metaContextOfGoal and GoalState.metaState

This replaces the sexp based interface for emitting structures. To facilitate this, the user has to execute `MetaM` monads. The state of this monad can be queried from any individual goal by `GoalState.metaContextOfGoal` and `GoalState.metaState`

aniva added the

part/Serial

category

feature

labels 2024-06-26 06:34:26 -07:00

aniva self-assigned this 2024-06-26 06:34:26 -07:00

aniva added 2 commits 2024-06-26 06:34:27 -07:00

feat: Condensed interface ffbea41f62

feat: Extract MetaM context and state from goal 8e78718447

aniva added a new dependency 2024-06-26 06:35:05 -07:00

#83 feat: Prograde tactics

aniva added 1 commit 2024-08-04 17:32:38 -07:00

feat: Expose project and leanPkgs in flake 64269868d5

aniva added 1 commit 2024-08-04 17:52:57 -07:00

feat: Move non package outputs to dependencies caac70f0cf

aniva added 1 commit 2024-08-14 01:21:25 -07:00

refactor: Remove export of Lean functions ... 0bc7bc5856

If the user wishes to use Lean functions, they should add the bindings manually.

aniva added 1 commit 2024-08-15 22:40:02 -07:00

refactor: Assign into its own tactic e943a4b065

aniva merged commit 56100a30af into dev 2024-08-15 22:41:59 -07:00

aniva deleted branch serial/expr 2024-08-15 22:41:59 -07:00

aniva referenced this pull request from a commit 2024-08-15 22:42:00 -07:00

Merge pull request 'feat: Condensed interface' (#85) from serial/expr into dev

aniva referenced this pull request 2024-08-31 19:50:54 -07:00

Move towards Expr based interface #84

aniva referenced this pull request 2024-08-31 19:54:12 -07:00

Enable direct expression evaluation in context #74

aniva added this to the v0.3 milestone 2024-09-08 14:27:12 -07:00

Sign in to join this conversation.

Reviewers

No reviewers

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 labels

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

v0.3

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

aniva

1 participant

Notifications

Subscribe

Due date

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

No due date set.

Blocks

#83 feat: Prograde tactics

aniva/Pantograph

Reference: aniva/Pantograph#85

No description provided.