@[reducible, inline]

abbrev Lean.Compiler.LCNF.Probe (α : Type u_1) (β : Type) : Type u_1

@[inline]

def Lean.Compiler.LCNF.Probe.map {α : Type u_1} {β : Type} (f : α → CompilerM β) : Probe α β

@[inline]

def Lean.Compiler.LCNF.Probe.filter {α : Type} (f : α → CompilerM Bool) : Probe α α

@[inline]

def Lean.Compiler.LCNF.Probe.sorted {α : Type} [Inhabited α] [LT α] [DecidableLT α] : Probe α α

@[inline]

def Lean.Compiler.LCNF.Probe.sortedBySize : Probe Decl (Nat × Decl)

def Lean.Compiler.LCNF.Probe.countUnique {α : Type} [ToString α] [BEq α] [Hashable α] : Probe α (α × Nat)

@[inline]

def Lean.Compiler.LCNF.Probe.countUniqueSorted {α : Type} [ToString α] [BEq α] [Hashable α] [Inhabited α] : Probe α (α × Nat)

def Lean.Compiler.LCNF.Probe.getLetValues : Probe Decl LetValue

partial def Lean.Compiler.LCNF.Probe.getLetValues.go (c : Code) : StateRefT' IO.RealWorld (Array LetValue) CompilerM Unit

def Lean.Compiler.LCNF.Probe.getLetValues.start (decls : Array Decl) : StateRefT' IO.RealWorld (Array LetValue) CompilerM Unit

def Lean.Compiler.LCNF.Probe.getJps : Probe Decl FunDecl

partial def Lean.Compiler.LCNF.Probe.getJps.go (code : Code) : StateRefT' IO.RealWorld (Array FunDecl) CompilerM Unit

def Lean.Compiler.LCNF.Probe.getJps.start (decls : Array Decl) : StateRefT' IO.RealWorld (Array FunDecl) CompilerM Unit

def Lean.Compiler.LCNF.Probe.filterByLet (f : LetDecl → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByLet.go (f : LetDecl → CompilerM Bool) : Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByFun (f : FunDecl → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByFun.go (f : FunDecl → CompilerM Bool) : Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByJp (f : FunDecl → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByJp.go (f : FunDecl → CompilerM Bool) : Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByFunDecl (f : FunDecl → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByFunDecl.go (f : FunDecl → CompilerM Bool) : Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByCases (f : Cases → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByCases.go (f : Cases → CompilerM Bool) : Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByJmp (f : FVarId → Array Arg → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByJmp.go (f : FVarId → Array Arg → CompilerM Bool) : Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByReturn (f : FVarId → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByReturn.go (f : FVarId → CompilerM Bool) : Code → CompilerM Bool

def Lean.Compiler.LCNF.Probe.filterByUnreach (f : Expr → CompilerM Bool) : Probe Decl Decl

partial def Lean.Compiler.LCNF.Probe.filterByUnreach.go (f : Expr → CompilerM Bool) : Code → CompilerM Bool

@[inline]

def Lean.Compiler.LCNF.Probe.declNames : Probe Decl Name

@[inline]

def Lean.Compiler.LCNF.Probe.toString {α : Type u_1} [ToString α] : Probe α String

@[inline]

def Lean.Compiler.LCNF.Probe.count {α : Type u_1} : Probe α Nat

@[inline]

def Lean.Compiler.LCNF.Probe.sum : Probe Nat Nat

@[inline]

def Lean.Compiler.LCNF.Probe.tail {α : Type} (n : Nat) : Probe α α

@[inline]

def Lean.Compiler.LCNF.Probe.head {α : Type} (n : Nat) : Probe α α

def Lean.Compiler.LCNF.Probe.runOnDeclsNamed {β : Type} (declNames : Array Name) (probe : Probe Decl β) (phase : Phase := Phase.base) : CoreM (Array β)

def Lean.Compiler.LCNF.Probe.runOnModule {β : Type} (moduleName : Name) (probe : Probe Decl β) (phase : Phase := Phase.base) : CoreM (Array β)

def Lean.Compiler.LCNF.Probe.runGlobally {β : Type} (probe : Probe Decl β) (phase : Phase := Phase.base) : CoreM (Array β)

def Lean.Compiler.LCNF.Probe.toPass {β : Type} [ToString β] (probe : Probe Decl β) (phase : Phase) : Pass