Documentation

Qq.AssertInstancesCommute

source
def Qq.termAssumeInstancesCommute'_ :
Lean.ParserDescr
Instances For
    source
    def Qq.Impl.isRedundantLocalInst? (inst : Lean.FVarId) :
    Lean.MetaM (Option Lean.Expr)
    Instances For
      source
      def Qq.Impl.findRedundantLocalInst? :
      Qq.Impl.QuoteM (Option (Lean.FVarId × Lean.Expr))
      Instances For
        source
        def Qq.Impl.findRedundantLocalInstQuoted? :
        Lean.Elab.TermElabM (Option (Lean.FVarId × (u : Q(Lean.Level)) × (ty : Q(Q(Sort «$u»))) × Q(Q(«$$ty»)) × Q(Q(«$$ty»))))
        Instances For
          source
          def Qq.Impl.termAssertInstancesCommuteImpl_ :
          Lean.ParserDescr
          Instances For
            source
            def Qq.Impl.termAssertInstancesCommuteDummy :
            Lean.ParserDescr
            Instances For
              source
              def Qq.Impl.termAssumeInstancesCommuteDummy :
              Lean.ParserDescr
              Instances For
                source
                def Qq.doElemAssertInstancesCommute :
                Lean.ParserDescr
                Instances For
                  source
                  def Qq.doElemAssumeInstancesCommute :
                  Lean.ParserDescr
                  Instances For