This media is not supported in your browser
VIEW IN TELEGRAM
Добавил в LSP ошибки
В начале эти inc inc тут как демонстрация отзывчивости шо каждая следующая на следующем i появляется
В начале эти inc inc тут как демонстрация отзывчивости шо каждая следующая на следующем i появляется
Чтобы AI не путали с AI, Apple ID переименовывают в Apple Account(у эпла теперь есть эпл интеллидженс)
Media is too big
VIEW IN TELEGRAM
#макмакич
не работает блять клавиши мыши назад вперед(4 5) в местном проводнике, и вообще проводник кал говна
Если открылась папка из какого то приложения попасть назад(`/..`) нельзя, клавиши вперед назад отвечают только за историю, а тк кк папка открылась из приложения история чистая
Можно ли тыкнуть сверху в путь чтобы попасть на папку выше как в винде и лине? НЕТ КОНЕЧНО
не работает блять клавиши мыши назад вперед(4 5) в местном проводнике, и вообще проводник кал говна
Если открылась папка из какого то приложения попасть назад(`/..`) нельзя, клавиши вперед назад отвечают только за историю, а тк кк папка открылась из приложения история чистая
Можно ли тыкнуть сверху в путь чтобы попасть на папку выше как в винде и лине? НЕТ КОНЕЧНО
В опросе языков могущих в proof assistant(в основном это значит типы первого порядка) с большим отрывом побеждает Lean
Вот определение натуральных чисел на нем
логика тут в рекурсивности, шото вроде либо это 0 либо оно само + 1, получается если много делать succ то можно получить любое натуральное число, а сам факт того шо они натуральные следует из того шо тут нет вычитания
Вот определение натуральных чисел на нем
inductive nat : Type
| zero : nat
| succ : nat → nat
def Nat.add : Nat → Nat → Nat
| n, Nat.zero => n // n + 0 = n
| n, Nat.succ m => Nat.succ (Nat.add n m) // n + succ(m) = succ(n + m)
логика тут в рекурсивности, шото вроде либо это 0 либо оно само + 1, получается если много делать succ то можно получить любое натуральное число, а сам факт того шо они натуральные следует из того шо тут нет вычитания
gavr_sas
Главная цель когда делаешь в яп эксепшоны, сделать их оутпут минимальным и понятным zero bullshit principle
заменил длинный еррор на короткий в случае если мы в LSP моде, надо бы так со всеми еррорами проделать, постепенно
👍1
Forwarded from Denis Rangelov 🦄