Provedalphaalpha-core-v0type-inference

Alpha Core v0: the fixture (identity applied to Nat and 1) infers Nat

\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{infer}}(\htmlData{mx=1}{\left[ \right]}, \htmlData{mx=2}{\operatorname{fixture}})} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{\htmlData{mx=4}{\operatorname{some}}(\htmlData{mx=5}{\operatorname{fixtureType}})}

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 [], fixture. Lean writes f x; papers write f(x). (infer [] fixture)
=Equality: infer([], fixture) and some(fixtureType) are the same. (infer [] fixture = some fixtureType)
[a, b]List: The list of , in order. ([])
fixture: fixture: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixture)
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)
fixtureType: fixtureType: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixtureType)

theorem alpha-core-v0-fixture-infers :
    infer [] fixture = some fixtureType

Type inference gives the frozen two-module fixture, (identity Nat) (successor zero), the type Nat 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: 7 lines of Lean