Documentation

Lean.Compiler.LCNF.Simp.Used

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

Equations
    Instances For

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

      Equations
        Instances For

          Mark all free variables occurring in arg as used.

          Equations
            Instances For

              Mark all free variables occurring in e as used.

              Equations
                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
                          <code>
                          
                          Equations
                            Instances For
                              @[irreducible]
                              Equations
                                Instances For