Function infer_type 

pub fn infer_type(ctx: &Context, term: &Term) -> KernelResult<Term>

Infer the type of a term in a context.

This is the main entry point for type checking. It implements bidirectional type inference for the Calculus of Constructions.

Type Rules

• Type n : Type (n+1) - Universes form a hierarchy
• x : A if x : A in context - Variable lookup
• Π(x:A). B : Type max(i,j) if A : Type i and B : Type j
• λ(x:A). t : Π(x:A). B if t : B in extended context
• f a : B[x := a] if f : Π(x:A). B and a : A

Errors

Returns KernelError variants for:

• Unbound variables
• Type mismatches in applications
• Invalid match constructs
• Termination check failures for fixpoints