Documentation

Lean.Meta.Instances

@[inline, reducible]
Equations
Instances For
    Instances For
    Equations
    Equations
    Equations
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Compute the order the arguments of inst should by synthesized.

          The synthesization order makes sure that all mvars in non-out-params of the subgoals are assigned before we try to synthesize it. Otherwise it goes left to right.

          For example:

          • [Add α] [Zero α] : Foo α returns [0, 1]
          • [Mul A] [Mul B] [MulHomClass F A B] : FunLike F A B returns [2, 0, 1] (because A B are out-params and are only filled in once we synthesize 2)

          (The type of inst must not contain mvars.)

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Lean.Meta.addInstance (declName : Lake.Name) (attrKind : Lean.AttributeKind) (prio : Nat) :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Default instance support #

                      Instances For
                        @[inline, reducible]
                        Equations
                        Instances For
                          Equations
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For