Documentation

Lean.Compiler.LCNF.Simp.Used

Mark fvarId as an used free variable. This is information is used to eliminate dead local declarations.

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

    Mark all free variables occurring in type as used. This is information is used to eliminate dead local declarations.

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

      Mark all free variables occurring in arg as used.

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

        Mark all free variables occurring in e as used.

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

          Mark all free variables occurring on the right-hand side of the given let declaration as used. This is information is used to eliminate dead local declarations.

          Equations
          Instances For

            Mark all free variables occurring in code as used.

            Mark all free variables occurring in funDecl as used.

            Return true if fvarId is in the used set.

            Equations
            Instances For

              Attach the given decls to code. For example, assume decls is #[.let _x.1 := 10, .let _x.2 := true], then the result is

              let _x.1 := 10
              let _x.2 := true
              
              
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For