Odomontois

import collection.immutable.TreeSet
object Solution {
    case class Item(cur: Int, next: List[Int], id: Int)
    implicit val itemOrdering: Ordering[Item] = Ordering.by(i => (i.cur,i.next.headOption, i.id))
    def go(s: TreeSet[Item]): LazyList[Vector[Int]] = 
       Vector(s.head.cur, s.last.cur) #:: (s.head match {
           case Item(_, x :: rest, id) => go(s.tail + Item(x, rest, id))
           case _ => LazyList.empty
       })   
    def smallestRange(nums: List[List[Int]]): Array[Int] =

Odomontois

# noinspection PyPep8Naming
class Solution:
    def ladderLength(self, beginWord: str, endWord: str, wordList: List[str]) -> int:
        d = defaultdict(list)
        for word in wordList:
            for i in range(len(word)):
                d[word[:i], word[i + 1:]].append(word)
        seen = {beginWord}
        q = [beginWord]
        steps = 1

Odomontois

import playground.chat.whatType


class BuznesErar
class ServesErar

def buznes: BiDyrka[BuznesErar, String] = BiDyrka.impl
def serves(s: String): BiDyrka[ServesErar, Int] = BiDyrka.impl

val x : BiDyrka[ServesErar | BuznesErar, Int] = 

Odomontois

\import Homotopy.Pointed

\data SmashProduct (X Y : Pointed)
  | spd X Y  -- "smash product data"
  | smashl (x : X) (i : I) \elim i {
    | left => spd x Y.base
    | right => spd X.base Y.base
  }
  | smashr (y : Y) (i : I) \elim i {
    | left => spd X.base y

Odomontois

\data Vect (n : Nat) (A : \Set)  \elim n
  | 0 => VNil
  | suc n => \infixr 5 :: A (Vect n A) \where {
  \func remove {n : Nat} {A : \Set} {a : A} (v : Vect (suc n) A) (i : Index a v) : Vect n A \elim n, v, i
    | n, :: b t, Here p => t
    | suc n, :: b t, There i => b :: remove t i
    | 0, :: _ VNil, There j => contradiction

  \lemma remove-here {n : Nat} {A : \Set} {a b : A} (t : Vect n A) (p : a = b) : remove (b :: t) (Here p) = t \elim n
    | n => idp

Odomontois

Поясняю за Mid по запросу @aleksei_t

Исходная мысль была такая. Итак у нас есть

trait MyBusinessModule[F[_]]{
  def doBusinessThing(entity: Entity, info: Info): F[Value]
  def undoBusinessThing(entity: Entity): F[Respect]
}

Odomontois

package scalagroup.tethys

import derevo.Derivation
import magnolia.{CaseClass, Magnolia, SealedTrait, Subtype}
import tethys.commons.Token
import tethys.readers.tokens.QueueIterator.WrongTokenError
import tethys.readers.tokens.{BaseTokenIterator, TokenIterator}
import tethys.readers.{FieldName, ReaderError}
import tethys.writers.tokens.TokenWriter
import tethys.{JsonReader, JsonWriter}

Odomontois

\data IO (A : \Set) : \Set (\suc \lp)
  | Input (A = Nat)
  | Output Nat (A = (\Sigma))

\func UnaryTC => \Set -> \Set (\suc \lp)

\data ITreeF (E : UnaryTC) (R : \Set) (X : \Type)
  | retF R
  | tauF X
  | visF {A : \Set} (event : E A) (k : A -> X)

Odomontois

{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DisambiguateRecordFields #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE NamedFieldPuns           #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE TypeFamilies             #-}

module MTG where

Odomontois

import magnolia.{CaseClass, Magnolia}
import ru.tinkoff.tschema.swagger.{DescribeTypeable, SwaggerDescription}
import cats.syntax.functorFilter._
import cats.syntax.functor._
import cats.instances.list._
import cats.instances.option._
import derevo.Derivation

import scala.annotation.StaticAnnotation