Documentation

Lake.Util.Binder

@[inline, reducible]
Equations
Instances For
    @[inline, reducible]
    Equations
    Instances For
      @[inline, reducible]
      Equations
      Instances For
        Equations
        @[inline, reducible]
        abbrev Lake.Hole :
        Equations
        Instances For
          @[inline, reducible]
          Equations
          Instances For
            @[inline, reducible]
            Equations
            Instances For
              Equations
              Instances For
                Equations
                Equations
                @[inline, reducible]
                Equations
                Instances For
                  @[inline, reducible]
                  Equations
                  Instances For
                    Equations
                    Instances For
                      @[inline, reducible]
                      Equations
                      Instances For
                        instance Lake.instCoeBinderTSyntaxConsSyntaxNodeKindIdentKindMkStr4Nil :
                        Coe Lake.Binder (Lean.TSyntax [Lean.identKind, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder])
                        Equations
                        @[inline, reducible]
                        Equations
                        Instances For
                          Equations
                          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
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    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
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For