Documentation

Lean.Compiler.LCNF.Simp.SimpValue

Try to simplify projections .proj _ i s where s is constructor.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Application over application.

    let g := f a
    g b
    

    is simplified to f a b.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Try to apply simple simplifications.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For