Skip to main content

normalize

oxilean_kernel::level::functions

Function normalize 

Source 
pub fn normalize(l: &Level) -> Level
Expand description

Normalize a universe level to canonical form.

Follows LEAN 4’s normalization algorithm:

  1. Flatten nested max expressions
  2. Normalize each argument recursively
  3. Sort arguments
  4. Merge duplicates (keep larger offsets)
  5. Remove subsumed explicit levels