Direct Imported Duplicates

 Direct Imported Duplicates🔗

Compiled2026-09-30T10:46:47ZProject4848fcaMerge pull request #481 from leanprover/chore/reconcile-v434-reference-pinsLeanleanprover/lean4:v4.34.1VersoBlueprint4848fca
Definition1
uses 0used by 0✓L∃∀N
Lean code for Definition1●1 definition
  • defdefined in VersoBlueprintTests/BlueprintImportedDuplicates/ProviderA.lean
    complete
    def Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeAVerso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA : Nat :
  NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

    def Verso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeAVerso.VersoBlueprintTests.BlueprintImportedDuplicates.ProviderA.importedNodeA : Nat :
  NatNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.