Documentation

Lean.Meta.Instances

@[reducible, inline]
Equations
    Instances For
      Instances For
        @[reducible, inline]
        Equations
          Instances For
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      def Lean.Meta.Instances.erase {m : TypeType} [Monad m] [MonadError m] (d : Instances) (declName : Name) :
                      Equations
                        Instances For
                          def Lean.Meta.addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) :
                          Equations
                            Instances For
                              def Lean.Meta.isInstanceCore (env : Environment) (declName : Name) :
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For

                                              Default instance support #

                                              Instances For
                                                @[reducible, inline]
                                                Equations
                                                  Instances For
                                                    Instances For
                                                      def Lean.Meta.addDefaultInstance (declName : Name) (prio : Nat := 0) :
                                                      Equations
                                                        Instances For
                                                          Equations
                                                            Instances For
                                                              def Lean.Meta.getDefaultInstances {m : TypeType} [Monad m] [MonadEnv m] (className : Name) :
                                                              m (List (Name × Nat))
                                                              Equations
                                                                Instances For