# Divergences from the Lean Kernel

This is a list of places where lean4lean deliberately has different behavior from the kernel. Unless specified here, any divergence between lean4lean and [lean4](https://github.com/leanprover/lean4/tree/master/src/kernel) is a bug.

* [`Lean4Lean.TypeChecker.Inner.reduceNative`](Lean4Lean/TypeChecker.lean): Lean4lean does not support reduction of `reduceBool`. This would involve implementing verified compilation, which while possible would be an additional chunk of work comparable to this entire repo.
* [`Lean4Lean.Environment.checkPrimitiveDef`](Lean4Lean/Primitive.lean), `checkPrimitiveInductive`: Lean does not check that primitives are declared with the correct types and definitional behavior, except in the case of `Eq` which is used in the declaration of `Quot`. This is required for soundness, but Lean is able to get away with it because Lean ships its prelude and using an alternative prelude is not supported.
* [`Lean4Lean.TypeChecker.Inner.inferType'`](Lean4Lean/TypeChecker.lean), literal case: The original code was not checking that the literal type actually exists. Again, this is okay provided that the prelude is trusted.
* [`Lean4Lean.TypeChecker.Inner.tryStringLitExpansionCore`](Lean4Lean/TypeChecker.lean): there is a counterproductive `whnf` call in this function which is removed in Lean4lean.
* [`Lean.Level.normalize'`](Lean4Lean/Level.lean), `isEquiv'`, `geq'`: Lean4lean implements an experimental new algorithm for level normalization, which is complete for level algebra. We may in the future use a hybrid approach avoid the performance cost in the common case.
* [`Lean4Lean.addDefinition`](Lean4Lean/Environment.lean), `Lean4Lean.addTheorem`: two calls ([1](https://github.com/leanprover/lean4/blob/v4.26.0/src/kernel/environment.cpp#L183) [2](https://github.com/leanprover/lean4/blob/v4.26.0/src/kernel/environment.cpp#L203)) are redundant and have been removed.
* [`Lean4Lean.TypeChecker.Inner.inferLambda`](Lean4Lean/TypeChecker.lean), `inferLet`: lean4lean does the `ensureSort` call before extending the context, while [`infer_lambda`](https://github.com/leanprover/lean4/blob/v4.26.0/src/kernel/type_checker.cpp#L124-L126) does it afterward. It's not clear whether this is actually unsound but it would require some very weird invariants to justify having unchecked things in the local context and hoping that they won't be used in the typing proof of that same expression.
* [`Lean4Lean.checkConstantVal`](Lean4Lean/Environment.lean): The original implementation would call `check` which sets the level params and then unsets them afterward, and then `ensure_sort` would run in a context without any level params. In lean4lean the monad is parameterized over level params, so they remain the same across the two calls.