HepLean Documentation

Lean.Compiler.LCNF.Simp.Used

source
def Lean.Compiler.LCNF.Simp.markUsedFVar (fvarId : Lean.FVarId) :
Lean.Compiler.LCNF.Simp.SimpM Unit

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
    source
    def Lean.Compiler.LCNF.Simp.markUsedType (type : Lean.Expr) :
    Lean.Compiler.LCNF.Simp.SimpM Unit

    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
      source
      def Lean.Compiler.LCNF.Simp.markUsedArg (arg : Lean.Compiler.LCNF.Arg) :
      Lean.Compiler.LCNF.Simp.SimpM Unit

      Mark all free variables occurring in arg as used.

      Equations
      Instances For
        source
        def Lean.Compiler.LCNF.Simp.markUsedLetValue (e : Lean.Compiler.LCNF.LetValue) :
        Lean.Compiler.LCNF.Simp.SimpM Unit

        Mark all free variables occurring in e as used.

        Equations
        Instances For
          source
          def Lean.Compiler.LCNF.Simp.markUsedLetDecl (letDecl : Lean.Compiler.LCNF.LetDecl) :
          Lean.Compiler.LCNF.Simp.SimpM Unit

          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
            source
            partial def Lean.Compiler.LCNF.Simp.markUsedCode (code : Lean.Compiler.LCNF.Code) :
            Lean.Compiler.LCNF.Simp.SimpM Unit

            Mark all free variables occurring in code as used.

            source
            partial def Lean.Compiler.LCNF.Simp.markUsedFunDecl (funDecl : Lean.Compiler.LCNF.FunDecl) :
            Lean.Compiler.LCNF.Simp.SimpM Unit

            Mark all free variables occurring in funDecl as used.

            source
            def Lean.Compiler.LCNF.Simp.isUsed (fvarId : Lean.FVarId) :
            Lean.Compiler.LCNF.Simp.SimpM Bool

            Return true if fvarId is in the used set.

            Equations
            Instances For
              source
              def Lean.Compiler.LCNF.Simp.attachCodeDecls (decls : Array Lean.Compiler.LCNF.CodeDecl) (code : Lean.Compiler.LCNF.Code) :
              Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.Code

              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
                source
                @[irreducible]
                def Lean.Compiler.LCNF.Simp.attachCodeDecls.go (decls : Array Lean.Compiler.LCNF.CodeDecl) (i : Nat) (code : Lean.Compiler.LCNF.Code) :
                Lean.Compiler.LCNF.Simp.SimpM Lean.Compiler.LCNF.Code
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For