Documentation

Lake.Util.Binder

source
@[reducible, inline]
abbrev Lake.Ellipsis :
Type
Instances For
    source
    @[reducible, inline]
    abbrev Lake.NamedArgument :
    Type
    Instances For
      source
      @[reducible, inline]
      abbrev Lake.Argument :
      Type
      Instances For
        source
        @[implicit_reducible]
        instance Lake.instCoeTermArgument :
        Coe Lean.Term Argument
        source
        @[implicit_reducible]
        instance Lake.instCoeEllipsisArgument :
        Coe Ellipsis Argument
        source
        @[implicit_reducible]
        instance Lake.instCoeNamedArgumentArgument :
        Coe NamedArgument Argument
        source
        @[reducible, inline]
        abbrev Lake.Hole :
        Type
        Instances For
          source
          @[reducible, inline]
          abbrev Lake.BinderIdent :
          Type
          Instances For
            source
            @[reducible, inline]
            abbrev Lake.TypeSpec :
            Type
            Instances For
              source
              def Lake.mkHoleFrom (ref : Lean.Syntax) :
              Hole

              Same as mkHole but returns TSyntax.

              Instances For
                source
                @[implicit_reducible]
                instance Lake.instCoeHoleTerm :
                Coe Hole Lean.Term
                source
                @[implicit_reducible]
                instance Lake.instCoeHoleBinderIdent :
                Coe Hole BinderIdent
                source
                @[implicit_reducible]
                instance Lake.instCoeIdentBinderIdent :
                Coe Lean.Ident BinderIdent
                source
                @[reducible, inline]
                abbrev Lake.BracketedBinder :
                Type
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Lake.FunBinder :
                  Type
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Lake.instCoeBinderIdentFunBinder :
                    Coe BinderIdent FunBinder
                    source
                    @[reducible, inline]
                    abbrev Lake.DeclBinder :
                    Type
                    Instances For
                      source
                      def Lake.binder :
                      Lean.Parser.Parser
                      Instances For
                        source
                        @[reducible, inline]
                        abbrev Lake.Binder :
                        Type
                        Instances For
                          source
                          @[implicit_reducible]
                          instance Lake.instCoeBinderIdentBinder :
                          Coe BinderIdent Binder
                          source
                          @[implicit_reducible]
                          instance Lake.instCoeBracketedBinderBinder :
                          Coe BracketedBinder Binder
                          source
                          @[implicit_reducible]
                          instance Lake.instCoeBinderDeclBinder :
                          Coe Binder DeclBinder
                          source
                          @[reducible, inline]
                          abbrev Lake.BinderModifier :
                          Type
                          Instances For
                            source
                            @[reducible, inline]
                            abbrev Lake.DepArrow :
                            Type
                            Instances For
                              source
                              @[implicit_reducible]
                              instance Lake.instCoeDepArrowTerm :
                              Coe DepArrow Lean.Term
                              source
                              structure Lake.BinderSyntaxView :
                              Type
                              Instances For
                                source
                                def Lake.instInhabitedBinderSyntaxView.default :
                                BinderSyntaxView
                                Instances For
                                  source
                                  @[implicit_reducible]
                                  instance Lake.instInhabitedBinderSyntaxView :
                                  Inhabited BinderSyntaxView
                                  source
                                  @[implicit_reducible]
                                  instance Lake.instReprBinderSyntaxView :
                                  Repr BinderSyntaxView
                                  source
                                  def Lake.instReprBinderSyntaxView.repr :
                                  BinderSyntaxView → Nat → Std.Format
                                  Instances For
                                    source
                                    def Lake.expandOptType (ref optType : Lean.Syntax) :
                                    Lean.Term
                                    Instances For
                                      source
                                      def Lake.getBinderIds (ids : Lean.Syntax) :
                                      Lean.MacroM (Array BinderIdent)
                                      Instances For
                                        source
                                        def Lake.expandBinderIdent (stx : Lean.Syntax) :
                                        Lean.MacroM Lean.Ident
                                        Instances For
                                          source
                                          def Lake.expandOptIdent (stx : Lean.Syntax) :
                                          BinderIdent
                                          Instances For
                                            source
                                            def Lake.expandBinderType (ref stx : Lean.Syntax) :
                                            Lean.Term
                                            Instances For
                                              source
                                              def Lake.expandBinderModifier (optBinderModifier : Lean.Syntax) :
                                              Option BinderModifier
                                              Instances For
                                                source
                                                def Lake.expandBinderCore (binders : Array BinderSyntaxView) (stx : Lean.Syntax) :
                                                Lean.MacroM (Array BinderSyntaxView)
                                                Instances For
                                                  source
                                                  @[inline]
                                                  def Lake.expandBinder (stx : Lean.Syntax) :
                                                  Lean.MacroM (Array BinderSyntaxView)
                                                  Instances For
                                                    source
                                                    def Lake.expandBinders (stxs : Array Lean.Syntax) :
                                                    Lean.MacroM (Array BinderSyntaxView)
                                                    Instances For
                                                      source
                                                      def Lake.BinderSyntaxView.mkBinder :
                                                      BinderSyntaxView → BracketedBinder
                                                      Instances For
                                                        source
                                                        def Lake.BinderSyntaxView.mkDepArrow (res : Lean.Term) (self : BinderSyntaxView) :
                                                        DepArrow
                                                        Instances For
                                                          source
                                                          def Lake.mkDepArrow (binders : Array BinderSyntaxView) (res : Lean.Term) :
                                                          Lean.Term
                                                          Instances For
                                                            source
                                                            def Lake.BinderSyntaxView.mkFunBinder :
                                                            BinderSyntaxView → FunBinder
                                                            Instances For
                                                              source
                                                              def Lake.BinderSyntaxView.mkArgument :
                                                              BinderSyntaxView → NamedArgument
                                                              Instances For