Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Initialize Lean project #1

Merged
merged 14 commits into from
Dec 28, 2023
Merged

Initialize Lean project #1

merged 14 commits into from
Dec 28, 2023

Conversation

eyihluyc
Copy link
Member

@eyihluyc eyihluyc commented Dec 28, 2023

This pull request initializes Lean4 formalization project. The focus of these initial commits is on establishing the project structure (which is still tentative) and introducing the minimal version of the calculus.
The following files were added:

  • Minimal directory
    • Сalculus.lean specifies representation of 𝜑-calculus terms in Lean and contains implementation of reductions to both weak head normal form and normal form
    • Еest.lean contains conversion of terms to String and evaluates reductions of objects
  • Extended directory, which is empty at the moment
  • lakefile.lean contains information dependencies and how to build a project
  • lake-manifest.json is auto-generated
  • lean-toolchain specifies version of lean4
  • PhiCalculus.lean is a build target

To-Do before merge:

  • get feedback on the project structure for improvements

PR-Codex overview

This PR focuses on adding the Minimal.Calculus module and implementing the Term and OptionalAttr types with their respective functions. It also includes a whnf function for weak head normal form evaluation and an nf function for normal form evaluation.

Detailed summary

  • Added Minimal.Calculus module
  • Implemented Attr, OptionalAttr, and Term types
  • Implemented functions mapObj, incLocatorsFrom, incLocators, substituteLocator, lookup, insert, whnf, and nf
  • Added ToString instances for OptionalAttr and Term
  • Updated README.md with installation instructions

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

@fizruk fizruk marked this pull request as ready for review December 28, 2023 14:29
@fizruk
Copy link
Collaborator

fizruk commented Dec 28, 2023

Slightly fixed package format and filenames, added CI workflow to build and generate docs, with caching. Once this PR is merged, documentation should be submitted to gh-pages branch, at which point we should enable Pages for this repository.

@eyihluyc eyihluyc merged commit 3b5891d into master Dec 28, 2023
2 checks passed
@fizruk fizruk deleted the setup branch December 28, 2023 14:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants