Higher inductive types

[ice1000]

Whoo-hoo!

Completely drop conditions now.

[codecov]

Codecov Report

Merging #669 (58020ab) into main (7439003) will decrease coverage by 0.21%.
The diff coverage is 84.25%.

@@             Coverage Diff              @@
##               main     #669      +/-   ##
============================================
- Coverage     78.74%   78.52%   -0.22%     
+ Complexity     2875     2858      -17     
============================================
  Files           260      260              
  Lines          9423     9426       +3     
  Branches       1167     1166       -1     
============================================
- Hits           7420     7402      -18     
- Misses         1382     1396      +14     
- Partials        621      628       +7     

Impacted Files	Coverage Δ
.../src/main/java/org/aya/concrete/stmt/TeleDecl.java	90.54% <ø> (ø)
...rc/main/java/org/aya/concrete/visitor/StmtOps.java	0.00% <0.00%> (ø)
base/src/main/java/org/aya/core/def/CtorDef.java	80.00% <ø> (ø)
...ase/src/main/java/org/aya/core/pat/PatMatcher.java	74.13% <0.00%> (-6.90%)	⬇️
base/src/main/java/org/aya/core/serde/SerPat.java	75.00% <ø> (-6.25%)	⬇️
...ase/src/main/java/org/aya/core/term/MatchTerm.java	12.50% <ø> (ø)
...rc/main/java/org/aya/core/visitor/DefConsumer.java	36.58% <0.00%> (-1.88%)	⬇️
...e/src/main/java/org/aya/core/visitor/Expander.java	31.57% <0.00%> (ø)
...src/main/java/org/aya/core/visitor/TermFolder.java	63.63% <0.00%> (+2.27%)	⬆️
base/src/main/java/org/aya/tyck/ExprTycker.java	86.77% <ø> (ø)
... and 31 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[ice1000]

I guess merge for now (sorry about Hoshino's commits)

bors r+

[bors]

Build succeeded:

• commit-check
• gradle-check