Implement K prelude in Lean 4 #4725

New issue

Copy link

New issue

Copy link

Open

Open

Implement K prelude in Lean 4#4725

Copy link

Labels

lean4-backend

Description

tothtamas28

opened on Jan 8, 2025

Issue body actions

Most functions in domains.md are hooked. We need to provide a manual implementation for those. (The function declarations can and should be generated automatically.)

Reactions are currently unavailable

Activity

1. tothtamas28

   added

   lean4-backend

   on Jan 8, 2025
2. automergerpr-permission-manager

   added 3 commits that reference this issue on Jan 20, 2025

   Add uninterpreted `Map` implementation to `Prelude.lean` (#4734)

   ...

   9be6e60

   Add uninterpreted `Set` implementation to `Prelude.lean` (#4738)

   ...

   e5a79fc

   Add uninterpreted `List` implementation to `Prelude.lean` (#4740)

   ...

   2ec5eec

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

Labels

lean4-backend

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions

• Open in GitHub Copilot app