Allow alternative environment initiation #167

New Issue

aniva · 2025-01-29T17:02:17-08:00

aniva commented

2025-01-29 17:02:17 -08:00

From Brando Miranda: It would be a good idea to allow the environment to initialize by providing a header:

import X
open X.Y
open scoped X.Z

From Brando Miranda: It would be a good idea to allow the environment to initialize by providing a header: ```lean import X open X.Y open scoped X.Z ```

aniva added this to the 0.3 milestone 2025-01-29 17:02:17 -08:00

aniva added the

labels 2025-01-29 17:02:17 -08:00

aniva self-assigned this 2025-01-29 17:02:17 -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#167