Documentation

Qq.SortLocalDecls

source
structure Qq.SortLocalDecls.Context :
Type
Instances For
    source
    structure Qq.SortLocalDecls.State :
    Type
    Instances For
      source
      @[inline, reducible]
      abbrev Qq.SortLocalDecls.M (α : Type) :
      Type
      Instances For
        source
        partial def Qq.SortLocalDecls.visitExpr (e : Lean.Expr) :
        Qq.SortLocalDecls.M Unit
        source
        partial def Qq.SortLocalDecls.visitLocalDecl (localDecl : Lean.LocalDecl) :
        Qq.SortLocalDecls.M Unit
        source
        def Qq.sortLocalDecls (localDecls : Array Lean.LocalDecl) :
        Lean.MetaM (Array Lean.LocalDecl)
        Instances For