Documentation

Lake.Build.Job

@[inline, reducible]
abbrev Lake.Job (α : Type u_1) :
Type u_1

A Lake job.

Equations
Instances For
    @[inline, reducible]
    abbrev Lake.JobM (α : Type) :

    The monad of Lake jobs.

    Equations
    Instances For
      @[inline, reducible]
      abbrev Lake.ResultM :

      The monad of a finished Lake job.

      Equations
      Instances For
        @[inline]
        Equations
        Instances For
          @[inline]
          Equations
          Instances For
            @[inline]
            def Lake.Job.await {α : Type} (self : Lake.Job α) :
            Equations
            Instances For
              @[inline]
              Equations
              Instances For
                @[inline]
                def Lake.Job.bindAsync {α : Type} {β : Type} (self : Lake.Job α) (f : αLake.SchedulerM (Lake.Job β)) :
                Equations
                Instances For
                  @[inline, reducible]
                  abbrev Lake.BuildJob (α : Type u_1) :
                  Type u_1

                  A Lake build job.

                  Equations
                  Instances For
                    @[inline]
                    Equations
                    Instances For
                      @[inline]
                      Equations
                      Instances For
                        @[inline]
                        Equations
                        Instances For
                          @[inline]
                          Equations
                          Instances For
                            @[inline]
                            def Lake.BuildJob.pure {α : Type u_1} (a : α) :
                            Equations
                            Instances For
                              Equations
                              @[inline]
                              def Lake.BuildJob.map {α : Type u_1} {β : Type u_1} (f : αβ) (self : Lake.BuildJob α) :
                              Equations
                              Instances For
                                Equations
                                @[inline]
                                def Lake.BuildJob.mapWithTrace {α : Type u_1} {β : Type u_1} (f : αLake.BuildTraceβ × Lake.BuildTrace) (self : Lake.BuildJob α) :
                                Equations
                                Instances For
                                  @[inline]
                                  Equations
                                  Instances For
                                    @[inline]
                                    Equations
                                    Instances For
                                      @[inline]
                                      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
                                              def Lake.BuildJob.seqWithAsync {α : Type} {β : Type} {γ : Type} (f : αβγ) (t1 : Lake.BuildJob α) (t2 : Lake.BuildJob β) :
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                Equations
                                                Instances For
                                                  Equations
                                                  Instances For