G
В определении
Size: a a a
2020 March 25
С
ты говорил код отправишь, а его нте
По этой теме, которую ты спрашиваешь, кода у меня нет. Скажи, что именно тебе нужно.
AZ
По этой теме, которую ты спрашиваешь, кода у меня нет. Скажи, что именно тебе нужно.
как мне через DI прокинуть коннект к постгрес базе
G
и какой он будет для списка [2,3,5,6,8,10]?
data GroupedList (step : Nat) -> Type where
constructor MkGroupedList
start : Int
count : Nat
Для примера выше будет
GroupedList 2.AZ
data GroupedList (step : Nat) -> Type where
constructor MkGroupedList
start : Int
count : Nat
Для примера выше будет
GroupedList 2.а как мы восстановим 2,3?
AZ
между ними шаг 1
С
как мне через DI прокинуть коннект к постгрес базе
Может быть не коннект, а генератор их? Который в
using(...) использоватьAZ
смотри
G
а как мы восстановим 2,3?
А, понял
AZ
[2,3,5,6,8,10, 20, 23, 30] -> [[2,3,5,6,8,10], [20,23], [30]]
AZ
А, понял
я о том и говорю
AZ
условие меняется незначительно, а этот подход оно ломает полностью
AZ
Может быть не коннект, а генератор их? Который в
using(...) использовать
AZ
вот я регистрирую ЕФ
AZ
что он дает: резолвит DataContext для всех типов что его запрашивают
AZ
теперь я хочу сделать такой же для постгрёвого клиента linq2db
AZ
для этого мне надо в AddTransient написать код который возвращает DataConnection или как он там
С
теперь я хочу сделать такой же для постгрёвого клиента linq2db
Ок, я как за комп вернусь, отвечу
AK
Короче, смысл в том, чтобы возвращать не
Тогда не придётся мучиться с доказательством того, что он возвращает списки упорядоченные по возрастанию через 1.
[[Int]], а [GroupedList], где GroupedList - этоrecord GroupedList where
constructor MkGroupedList
start : Int
count : Nat
Тогда не придётся мучиться с доказательством того, что он возвращает списки упорядоченные по возрастанию через 1.
По хорошему бинарный предикат может быть произвольным. Он должен передаваться первым аргом функции.
G
я о том и говорю
Тогда можно
Element определить как начальное значение и список шагов, а GroupedList как [Element] 🤦♀️