5eqn / proof-cat Goto Github PK

Constraint that param type and Pi destination must be U cannot be seen from placeholders. Consider adding type annotation for these placeholders.

Consider running test coverage in CI and show as a badge.

The type hint here shows undefined. The infer result is correct, the problem is only in type hint.

In src/typecheck/infer/pi.test.ts, the test infers type of (a: A) -> a, where a is not a type. This should throw ASTMismatch when checking a: U, because A is different from U. The test expects the Pi term's inferred type to be U, which is incorrect.

All inputs only render 1 character, this is insufficient for large-scaled usage.

Current error message only shows the root cause, which is typically unification error. Showing direct cause is perhaps more user-friendly.

Currently I use JetBrains Mono as monospace font, but the font family varies with clients, leading to inconsistency.

Consider adding a language switch.

Create React App ships with deprecated dependencies. Consider using Next.js, Vite or other actively-maintained frameworks.

Website freezes (for about 0.5 seconds) randomly. Consider doing some profiling.

state/ and view/ folder requires refactoring.

Consider supporting editing the default values of template blocks.