aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
281 stars 16 forks source link

Unify Signature with AbstractTele.Locns #1122

Closed HoshinoTented closed 4 months ago

HoshinoTented commented 4 months ago

Signature has a similar structure to AbstractTele.Locns, this PR intends to unify them.

Status: almost done, except class.

codecov[bot] commented 4 months ago

Codecov Report

Attention: Patch coverage is 91.66667% with 6 lines in your changes missing coverage. Please review.

Project coverage is 79.12%. Comparing base (4328b18) to head (a240b18). Report is 9 commits behind head on main.

:exclamation: Current head a240b18 differs from pull request most recent head 568bfc5

Please upload reports for the commit 568bfc5 to get more accurate results.

Files Patch % Lines
base/src/main/java/org/aya/tyck/StmtTycker.java 93.75% 1 Missing and 1 partial :warning:
...in/java/org/aya/syntax/telescope/AbstractTele.java 86.66% 0 Missing and 2 partials :warning:
.../src/main/java/org/aya/tyck/tycker/TeleTycker.java 80.00% 0 Missing and 1 partial :warning:
.../main/java/org/aya/syntax/telescope/Signature.java 90.00% 0 Missing and 1 partial :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #1122 +/- ## ============================================ - Coverage 79.17% 79.12% -0.06% + Complexity 3300 3292 -8 ============================================ Files 302 302 Lines 10012 10034 +22 Branches 1192 1195 +3 ============================================ + Hits 7927 7939 +12 - Misses 1425 1432 +7 - Partials 660 663 +3 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.