Documentation

Lake.Util.Binder

source
@[inline, reducible]
abbrev Lake.Ellipsis :
Type
Instances For
    source
    @[inline, reducible]
    abbrev Lake.NamedArgument :
    Type
    Instances For
      source
      @[inline, reducible]
      abbrev Lake.Argument :
      Type
      Instances For
        source
        instance Lake.instCoeTermArgument :
        Coe Lean.Term Lake.Argument
        source
        instance Lake.instCoeEllipsisArgument :
        Coe Lake.Ellipsis Lake.Argument
        source
        instance Lake.instCoeNamedArgumentArgument :
        Coe Lake.NamedArgument Lake.Argument
        source
        @[inline, reducible]
        abbrev Lake.Hole :
        Type
        Instances For
          source
          @[inline, reducible]
          abbrev Lake.BinderIdent :
          Type
          Instances For
            source
            @[inline, reducible]
            abbrev Lake.TypeSpec :
            Type
            Instances For
              source
              def Lake.mkHoleFrom (ref : Lean.Syntax) :
              Lake.Hole
              Instances For
                source
                instance Lake.instCoeHoleTerm :
                Coe Lake.Hole Lean.Term
                source
                instance Lake.instCoeHoleBinderIdent :
                Coe Lake.Hole Lake.BinderIdent
                source
                instance Lake.instCoeIdentBinderIdent :
                Coe Lean.Ident Lake.BinderIdent
                source
                @[inline, reducible]
                abbrev Lake.BracketedBinder :
                Type
                Instances For
                  source
                  @[inline, reducible]
                  abbrev Lake.FunBinder :
                  Type
                  Instances For
                    source
                    instance Lake.instCoeBinderIdentFunBinder :
                    Coe Lake.BinderIdent Lake.FunBinder
                    source
                    def Lake.binder :
                    Lean.Parser.Parser
                    Instances For
                      source
                      @[inline, reducible]
                      abbrev Lake.Binder :
                      Type
                      Instances For
                        source
                        instance Lake.instCoeBinderTSyntaxConsSyntaxNodeKindIdentKindMkStr4Nil :
                        Coe Lake.Binder (Lean.TSyntax [Lean.identKind, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder])
                        source
                        @[inline, reducible]
                        abbrev Lake.BinderModifier :
                        Type
                        Instances For
                          source
                          structure Lake.BinderSyntaxView :
                          Type
                          Instances For
                            source
                            def Lake.expandOptType (ref : Lean.Syntax) (optType : Lean.Syntax) :
                            Lean.Term
                            Instances For
                              source
                              def Lake.getBinderIds (ids : Lean.Syntax) :
                              Lean.MacroM (Array Lake.BinderIdent)
                              Instances For
                                source
                                def Lake.expandBinderIdent (stx : Lean.Syntax) :
                                Lean.MacroM Lean.Ident
                                Instances For
                                  source
                                  def Lake.expandOptIdent (stx : Lean.Syntax) :
                                  Lake.BinderIdent
                                  Instances For
                                    source
                                    def Lake.expandBinderType (ref : Lean.Syntax) (stx : Lean.Syntax) :
                                    Lean.Term
                                    Instances For
                                      source
                                      def Lake.expandBinderModifier (optBinderModifier : Lean.Syntax) :
                                      Option Lake.BinderModifier
                                      Instances For
                                        source
                                        def Lake.matchBinder (stx : Lean.Syntax) :
                                        Lean.MacroM (Array Lake.BinderSyntaxView)
                                        Instances For
                                          source
                                          def Lake.BinderSyntaxView.mkBinder :
                                          Lake.BinderSyntaxView → Lean.MacroM Lake.Binder
                                          Instances For
                                            source
                                            def Lake.BinderSyntaxView.mkArgument :
                                            Lake.BinderSyntaxView → Lean.MacroM Lake.NamedArgument
                                            Instances For
                                              source
                                              def Lake.expandBinders (dbs : Array Lake.Binder) :
                                              Lean.MacroM (Array Lake.Binder × Array Lean.Term)
                                              Instances For