feat: Add definitions and theorems to the environment #41

Merged

aniva merged 9 commits from env/add-decl into dev 2023-12-26 12:41:02 -08:00

Conversation 0 Commits 9 Files changed 10 +188 -90

aniva commented 2023-12-13 19:36:22 -08:00

Owner

Copy link

No description provided.

aniva added this to the v0.3 milestone 2023-12-13 19:36:22 -08:00

aniva added the

category

feature

part/Environment

labels 2023-12-13 19:36:22 -08:00

aniva self-assigned this 2023-12-13 19:36:22 -08:00

aniva added 2 commits 2023-12-13 19:36:23 -08:00

chore: Rename lib. commands to env. ... 12544b81ee

This is done to improve clarity and align with Lean's terminology

feat: env_add command 02889510b2

aniva added 1 commit 2023-12-14 05:51:00 -08:00

Merge branch 'dev' into env/add-decl 09f5792d4a

aniva added 1 commit 2023-12-14 05:52:29 -08:00

fix: env_add monads 2f3a91562a

aniva added 2 commits 2023-12-15 10:09:54 -08:00

test: env.add 6c25cca46a

fix: Force instantiate all mvars in env.add 3b83c81540

aniva added 2 commits 2023-12-15 10:40:56 -08:00

refactor: env. operations into its own file aca7dc9811

chore: Move environment functions to its own file ... 22789436bd

Symbol.lean is now subsumed

aniva added 1 commit 2023-12-26 12:27:04 -08:00

refactor: Rename Test/{Catalog,Environment} 77232d5a1e

aniva merged commit 6e39b5ef8b into dev 2023-12-26 12:41:02 -08:00

aniva deleted branch env/add-decl 2023-12-26 12:41:02 -08:00

aniva referenced this pull request from a commit 2023-12-26 12:41:02 -08:00

Merge pull request 'feat: Add definitions and theorems to the environment' (#41) from env/add-decl into dev

aniva referenced this pull request 2023-12-26 12:46:33 -08:00

Allow adding definitions to environments #1

aniva referenced this pull request from a commit 2024-04-11 15:44:02 -07:00

Merge pull request 'feat: Add definitions and theorems to the environment' (#41) from env/add-decl into dev

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.

Dependencies

No dependencies set.

Reference: aniva/Pantograph#41

No description provided.