Module primitive_wf 

Validating the well-founded Nat primitives: Nat.div, Nat.mod, Nat.gcd, Nat.bitwise.

These are defined by fuel or by WellFounded.fix, so their defining equations are not definitional for a symbolic argument the way Nat.add’s are. Following lean4lean’s Primitive.lean, the kernel instead checks, over free variables:

• the decision procedures they branch on (Nat.decLe, Nat.decEq, Bool.decEq) reflect their Boolean counterparts (Nat.ble, Nat.beq), so if/dite on them compute like the corresponding literal comparison;
• Nat.div/Nat.mod unfold, one fuel step at a time, to exactly the recursion of division;
• Nat.gcd/Nat.bitwise unfold through WellFounded.Nat.fix to the right-hand sides of their eq_def equations, whose fuel is always sufficient.

The reference terms these checks are stated with were elaborated by the pinned Lean toolchain (primitive_refs/PrimitiveRefs.lean), so no elaborated shape is reconstructed by hand.