Documentation

Qq.SortLocalDecls

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