Let Term

[HoshinoTented]

• Let Term and normalization
• Nested interface for nested structure
• LetPrettier for prettying let-like things

TODO:

• rendering the type of the bind during rendering LetTerm. I may use Synthesizer, but where does the TyckState come from?

[codecov]

Codecov Report

Merging #979 (efb446d) into main (7fb9a1b) will decrease coverage by 0.48%.
The diff coverage is 81.96%.

❗ Current head efb446d differs from pull request most recent head 74f77c9. Consider uploading reports for the commit 74f77c9 to get more accurate results

@@             Coverage Diff              @@
##               main     #979      +/-   ##
============================================
- Coverage     81.98%   81.50%   -0.48%     
+ Complexity     3475     3460      -15     
============================================
  Files           280      284       +4     
  Lines         10509    10557      +48     
  Branches       1271     1271              
============================================
- Hits           8616     8605      -11     
- Misses         1176     1223      +47     
- Partials        717      729      +12     

Impacted Files	Coverage Δ
base/src/main/java/org/aya/core/term/Term.java	89.58% <ø> (ø)
base/src/main/java/org/aya/ref/GenerateKind.java	75.00% <0.00%> (-25.00%)	⬇️
...e/src/main/java/org/aya/prettier/CorePrettier.java	67.75% <16.66%> (-11.33%)	⬇️
base/src/main/java/org/aya/core/term/LetTerm.java	85.71% <85.71%> (ø)
...se/src/main/java/org/aya/prettier/LetPrettier.java	87.50% <87.50%> (ø)
base/src/main/java/org/aya/concrete/Expr.java	86.26% <90.00%> (+0.21%)	⬆️
base/src/main/java/org/aya/core/serde/SerTerm.java	81.37% <100.00%> (+0.37%)	⬆️
...e/src/main/java/org/aya/core/serde/Serializer.java	86.71% <100.00%> (+0.21%)	⬆️
...c/main/java/org/aya/core/visitor/BetaExpander.java	74.00% <100.00%> (+0.53%)	⬆️
base/src/main/java/org/aya/generic/Nested.java	100.00% <100.00%> (ø)
... and 3 more

... and 10 files with indirect coverage changes

[ice1000]

Very nice! I'll go make some minor edits and merge this.

Gj!

[HoshinoTented]

😢

[HoshinoTented]

What's wrong? Consider term[x |-> y] where term or y contains z and we have a defEq z |-> x, the substituted term still has x after normalization. And this sounds very hard to solve...

So I suspend this PR.

Possible solution: learn from Arend

[HoshinoTented]

This feature may cost more than its benefit...