Module primitive 

Primitive validation: the literal extension is only as sound as the definitions it replaces.

Lean’s kernel evaluates Nat.add 2 3 on machine numbers instead of unfolding Nat.add. That is sound only if the environment’s Nat.add really is addition. Before a primitive name is admitted, its definition is checked against its defining equations, stated over a free variable so they hold for every argument (the scheme of lean4lean’s Primitive.lean). A primitive whose equations are proven is accelerated; one whose form is wrong is rejected.