Documentation

Qq.AssertInstancesCommute

source
def Qq.termAssumeInstancesCommute'_ :
Lean.ParserDescr
Equations
    Instances For
      source
      def Qq.Impl.isRedundantLocalInst? (inst : Lean.FVarId) :
      Lean.MetaM (Option Lean.Expr)
      Equations
        Instances For
          source
          def Qq.Impl.findRedundantLocalInst? :
          QuoteM (Option (Lean.FVarId × Lean.Expr))
          Equations
            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»))))
              Equations
                Instances For
                  source
                  def Qq.Impl.termAssertInstancesCommuteImpl_ :
                  Lean.ParserDescr
                  Equations
                    Instances For
                      source
                      def Qq.Impl.termAssertInstancesCommuteDummy :
                      Lean.ParserDescr
                      Equations
                        Instances For
                          source
                          def Qq.Impl.termAssumeInstancesCommuteDummy :
                          Lean.ParserDescr
                          Equations
                            Instances For
                              source
                              def Qq.doElemAssertInstancesCommute :
                              Lean.ParserDescr
                              Equations
                                Instances For
                                  source
                                  def Qq.doElemAssumeInstancesCommute :
                                  Lean.ParserDescr
                                  Equations
                                    Instances For