Provedalphaalpha-core-v0type-inferencequantitative-types
Alpha Core v0: the quantitative polymorphic identity infers Π⁰(A : U₀). Π¹(value : A). A
What the notation means · or point at any symbol
- infer
- infer: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
infer) - f(x)Function application
- infer applied to [], identity. Lean writes f x; papers write f(x). (
infer [] identity) - =Equality
- infer([], identity) and some(pi(erased)) are the same. (
infer [] identity = some (Term.pi Quant…) - [a, b]List
- The list of , in order. (
[]) - identity
- identity: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
identity) - some
- some: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
some) - pi
- Term.pi: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Term.pi) - erased
- Quantity.erased: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Quantity.erased)
theorem alpha-core-v0-identity-infers :
infer [] identity = some (Term.pi Quantity.erased "A" (Term.universe 0) (Term.pi Quantity.linear "value" (Term.variable "A") (Term.variable "A")))Type inference of Alpha Core v0 gives the identity function, whose type argument is erased (quantity 0) and whose value argument is linear (quantity 1), the type (0 A : Type 0) → (1 value : A) → A in the empty context.
How it was proved
- Proved
- 21 October 2026
- By
- Ajax
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 8 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.