Documentation

Qq.SortLocalDecls

← Copula mathematical handbook
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
        • One or more equations did not get rendered due to their size.
        Instances For