Let Term

[HoshinoTented]

• [x] Let Term and normalization
• [x] Nested interface for nested structure
• [x] 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[bot]]

Codecov Report

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

:exclamation: 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%)	:arrow_down:
...e/src/main/java/org/aya/prettier/CorePrettier.java	67.75% <16.66%> (-11.33%)	:arrow_down:
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%)	:arrow_up:
base/src/main/java/org/aya/core/serde/SerTerm.java	81.37% <100.00%> (+0.37%)	:arrow_up:
...e/src/main/java/org/aya/core/serde/Serializer.java	86.71% <100.00%> (+0.21%)	:arrow_up:
...c/main/java/org/aya/core/visitor/BetaExpander.java	74.00% <100.00%> (+0.53%)	:arrow_up:
base/src/main/java/org/aya/generic/Nested.java	100.00% <100.00%> (ø)
... and 3 more

... and 10 files with indirect coverage changes

[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...