structure Qq.SortLocalDecls.Context : Type

• localDecls : Lean.NameMap Lean.LocalDecl

structure Qq.SortLocalDecls.State : Type

• visited : Lean.NameSet
• result : Array Lean.LocalDecl

@[inline, reducible]

abbrev Qq.SortLocalDecls.M (α : Type) : Type

Equations

• Qq.SortLocalDecls.M = ReaderT Qq.SortLocalDecls.Context (StateRefT' IO.RealWorld Qq.SortLocalDecls.State Lean.MetaM)

partial def Qq.SortLocalDecls.visitExpr (e : Lean.Expr) : Qq.SortLocalDecls.M Unit

partial def Qq.SortLocalDecls.visitLocalDecl (localDecl : Lean.LocalDecl) : Qq.SortLocalDecls.M Unit

def Qq.sortLocalDecls (localDecls : Array Lean.LocalDecl) : Lean.MetaM (Array Lean.LocalDecl)

Equations

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