Documentation

Lean.Compiler.LCNF.Simp.Used

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

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

Instances For
    source
    def Lean.Compiler.LCNF.Simp.markUsedArg (arg : Arg Purity.pure) :
    SimpM Unit

    Mark all free variables occurring in arg as used.

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

      Mark all free variables occurring in e as used.

      Instances For
        source
        def Lean.Compiler.LCNF.Simp.markUsedLetDecl (letDecl : LetDecl Purity.pure) :
        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.

        Instances For
          source
          partial def Lean.Compiler.LCNF.Simp.markUsedCode (code : Code Purity.pure) :
          SimpM Unit

          Mark all free variables occurring in code as used.

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

          Mark all free variables occurring in funDecl as used.

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

          Return true if fvarId is in the used set.

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

            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>
            Instances For