We're almost there! We can use this PR to finish up work on getting all of the prelude to typecheck, as well as to do any finishing touches (refactors etc.). So far:
Adds primitive Nat.decLt and Nat.decLe operations.
Adds support for typechecking partial definitions (including those within mutual blocks).
Refactors the original NbE bidirectional checking system to be more like the typechecker that Lean itself uses, in particular check now simply infers and checks, and infer handles every case (including lambdas). This ensures that we correctly handle the case of applied lambdas (i.e. redexes), which are infrequent but do indeed occur throughout the Lean stdlib.
We're almost there! We can use this PR to finish up work on getting all of the prelude to typecheck, as well as to do any finishing touches (refactors etc.). So far:
Nat.decLtandNat.decLeoperations.checknow simply infers and checks, andinferhandles every case (including lambdas). This ensures that we correctly handle the case of applied lambdas (i.e. redexes), which are infrequent but do indeed occur throughout the Lean stdlib.