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

Fix two issues related to arrays and meta lit terms, implement `debug-show-shapes` #1147

Closed ice1000 closed 1 day ago

ice1000 commented 1 day ago

As title

codecov[bot] commented 1 day ago

Codecov Report

Attention: Patch coverage is 70.58824% with 5 lines in your changes missing coverage. Please review.

Project coverage is 79.84%. Comparing base (4b35a0d) to head (66cb8a2). Report is 8 commits behind head on main.

Files with missing lines Patch % Lines
base/src/main/java/org/aya/tyck/ExprTycker.java 72.72% 0 Missing and 3 partials :warning:
...se/src/main/java/org/aya/normalize/Normalizer.java 50.00% 1 Missing :warning:
...ain/java/org/aya/cli/interactive/ReplCompiler.java 0.00% 1 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #1147 +/- ## ============================================ - Coverage 79.86% 79.84% -0.03% - Complexity 3393 3397 +4 ============================================ Files 312 312 Lines 10232 10245 +13 Branches 1220 1225 +5 ============================================ + Hits 8172 8180 +8 - Misses 1392 1395 +3 - Partials 668 670 +2 ```

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

ice1000 commented 1 day ago

-0.03 is good enough