LeanMachineLearning

4.9. Tactic.EqLift.Tactic.Kernel.Utils🔗

Kernel lifting utilities

This file provides helper functions for lifting and unlifting kernel expressions, including type extraction and equivalence construction.

Main declarations

  • getTypesFromKernel: extracts carrier types and universe levels from kernel expressions.

  • constructMeasurableEquiv: recursively builds measurable equivalences.

  • getOriginalType: retrieves the original type from a lifted type.

Module LeanMachineLearning.Tactic.EqLift.Tactic.Kernel.Utils contains 4 exposed declarations.