Prove Expr.typeCheck_complete for full language with Var, Lam, App#8

Open

Copilot wants to merge 8 commits intomainfrom

copilot/prove-expr-typecheck-complete

Commits on Mar 1, 2026

Initial plan
Copilot
committed
Restore full intrinsically-typed expression language and prove typeCheck_complete

Copilot
and
Copilot
committed
Fix Props/Compiler.lean exhaustive cases and use Typ.Fn.injEq in HasType.det

Copilot
and
nahcnuj
committed

Commits on Mar 3, 2026

Fix CI failures in Props/Typing.lean and Props/Compiler.lean

Copilot
and
nahcnuj
committed

Commits on Mar 4, 2026

Commits on Mar 6, 2026

Add TODO comments to Compiler.lean and update README syntax with Var/Lam/App

Copilot
and
nahcnuj
committed