Allow adding definitions to environments #1

New Issue

aniva · 2023-08-21T19:53:21-07:00

aniva commented

2023-08-21 19:53:21 -07:00

There should be a way to add new definitions to an existing environment.

aniva added this to the 0.2.6 milestone 2023-08-21 19:53:21 -07:00

aniva added the

category

feature

label 2023-08-21 19:53:21 -07:00

aniva self-assigned this 2023-08-21 19:53:21 -07:00

aniva added the

part/Environment

label 2023-08-22 10:00:39 -07:00

aniva modified the milestone from 0.2.6 to 0.3

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

aniva commented

2023-11-07 16:49:47 -08:00

See https://github.com/leanprover/lean4/pull/2642. Use Environment.addDecl

See https://github.com/leanprover/lean4/pull/2642. Use `Environment.addDecl`

aniva commented

2023-12-26 12:46:33 -08:00

#41 solved

aniva closed this issue

2023-12-26 12:46:33 -08:00

Sign in to join this conversation.

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#1