Documentation

Lean.Meta.SortLocalDecls

structure Lean.Meta.SortLocalDecls.Context :

Type

localDecls : Lean.NameMap Lean.LocalDecl

structure Lean.Meta.SortLocalDecls.State :

Type

visited : Lean.NameSet
result : Array Lean.LocalDecl

@[inline]

abbrev Lean.Meta.SortLocalDecls.M (α : Type) :

Type

Equations

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

partial def Lean.Meta.SortLocalDecls.visitExpr (e : Lean.Expr) :

Lean.Meta.SortLocalDecls.M Unit

partial def Lean.Meta.SortLocalDecls.visitLocalDecl (localDecl : Lean.LocalDecl) :

Lean.Meta.SortLocalDecls.M Unit

def Lean.Meta.sortLocalDecls (localDecls : Array Lean.LocalDecl) :

Lean.MetaM (Array Lean.LocalDecl)

Equations

Lean.Meta.sortLocalDecls localDecls = let aux := do Array.forM Lean.Meta.SortLocalDecls.visitLocalDecl localDecls 0 (Array.size localDecls) let a ← get pure a.result; StateRefT'.run' (ReaderT.run aux { localDecls := Array.foldl (fun s d => Lean.NameMap.insert s (Lean.LocalDecl.fvarId d).name d) ∅ localDecls 0 (Array.size localDecls) }) { visited := ∅, result := #[] }