-
Notifications
You must be signed in to change notification settings - Fork 21
Locally nameless STLC #17
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
Locally nameless STLC #17
Conversation
Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Context.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
Outdated
Show resolved
Hide resolved
After this is merged, while we don't have any other PRs pending, I'm going to address all the outstanding lints so we can start with a clean slate. Could you take a look at the YAML for the lints workflow? I think there is an issue as I'm getting emails that say |
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Thanks for fixing the lint YAML file, seems to be running now. Looking at the output however, it is not catching the lint errors I see locally. I see these messages on the latest run:
|
Maybe it's got something to do with the version? I'm now using the same they use in mathlib. Otherwise, it might be that we should provide that script?.. |
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
Outdated
Show resolved
Hide resolved
Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
Outdated
Show resolved
Hide resolved
* first pass at STLC, should consider splitting this file * structure * progress * minimize imports * docs typo * docs * docs * remove redundant lemma * style * style * eliminate private lemma * eliminate private lemma * scope safety theorems * STLC namespace * restructure for clarity * reverse directory structure * paramaterize Ty base a base type * rm unused notation * naming convention * nicer speelling of Ctx.dom * rm terminal refine * style * use Data.List.Sigma * use HasWellFormed notation * Ctx -> Context * no space before ✓ * link/reference formatting * indent inductives * Context name convention * naming conventions * style * naming conventions * style
* first pass at STLC, should consider splitting this file * structure * progress * minimize imports * docs typo * docs * docs * remove redundant lemma * style * style * eliminate private lemma * eliminate private lemma * scope safety theorems * STLC namespace * restructure for clarity * reverse directory structure * paramaterize Ty base a base type * rm unused notation * naming convention * nicer speelling of Ctx.dom * rm terminal refine * style * use Data.List.Sigma * use HasWellFormed notation * Ctx -> Context * no space before ✓ * link/reference formatting * indent inductives * Context name convention * naming conventions * style * naming conventions * style
This PR adds simple typing derivations for locally nameless terms, with proofs of progress and preservation.
I have also reversed the directory structure of
LambdaCalculus
to be the representation then the system, e.g.{LocallyNameless,Named}/{Untyped,STLC}
. This matches the namespaces we have been using and better groups together related code.