Сейчас я изучаю, Agda.

Сейчас я изучаю, Agda.

а с лиспом дружишь?

Понятно ) Какая-то ультра-специфическая штука для избранных )

Минуточку, это и есть код :) Такой вот модуль: module eq where open import level data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where refl : x ≡ x infix 3 _≡_ sym : ∀ {ℓ}{A : Set ℓ}{x y : A} → x ≡ y → y ≡ x sym refl = refl trans : ∀ {ℓ}{A : Set ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ z trans refl refl = refl cong : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(p : A → B) {x y : A} → x ≡ y → p x ≡ p y cong p refl = refl cong-pred : ∀ {ℓ ℓ'}{A : Set ℓ}(P : A → Set ℓ') {x y : A} → x ≡ y → P x → P y cong-pred P refl p = p

Ну... просто программисты на Haskell решили, что Haskell иногда недостаточно функционален, и написали Agda, которая транслируется в Haskell, то с зависимыми типами и теоремами (изоморфизм Карри-Говарда).

эзотерикой пахнет

Звучит как что-то для подготовленных программистов )

Разве только математически. Во всяком случае мне интересно, отвлекает от ширпотреба на работе :)

Ну да, это и подразумеваю ) У нас вон много кодеров без образования, и ещё больше просто не хотят получать высшее, но хотят 300кк/нсек )

У меня нет высшего образования, и тоже не откажусь :)

Минуточку, это и есть код :) Такой вот модуль: module eq where open import level data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where refl : x ≡ x infix 3 _≡_ sym : ∀ {ℓ}{A : Set ℓ}{x y : A} → x ≡ y → y ≡ x sym refl = refl trans : ∀ {ℓ}{A : Set ℓ}{x y z : A} → x ≡ y → y ≡ z → x ≡ z trans refl refl = refl cong : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(p : A → B) {x y : A} → x ≡ y → p x ≡ p y cong p refl = refl cong-pred : ∀ {ℓ ℓ'}{A : Set ℓ}(P : A → Set ℓ') {x y : A} → x ≡ y → P x → P y cong-pred P refl p = p

А математика сама в голове нарисовалась? )

Единственное что мне тут знаком так это математические знаки для множеств)

https://roadmap.sh/frontend

Ребят👉👈 Короче я всех друзей нахер послал и серьёзно сел решать Пока об каждый камень спотыкаюсь, например: почему в HTML нельзя вставлять ссылку на картинку в <img> с сайта любого? Как в примере: https://vk.com/feed?z=photo-88245281_459977429%2Fwall-88245281_7885992 не бачит просто

Вот код, не бачит картинку выводить

Вот код, не бачит картинку выводить

Вот код, не бачит картинку выводить

Ребят👉👈 Короче я всех друзей нахер послал и серьёзно сел решать Пока об каждый камень спотыкаюсь, например: почему в HTML нельзя вставлять ссылку на картинку в <img> с сайта любого? Как в примере: https://vk.com/feed?z=photo-88245281_459977429%2Fwall-88245281_7885992 не бачит просто

https://sun4-16.userapi.com/impg/HKIQ6qxwxw4a4PGlcrIjWSRD8D8oUi5hd-C4_Q/triIN1V4hjY.jpg?size=1080x930&quality=96&sign=2fcbb89bfed4e047f48e7a074ffd94ce&type=album Вот у тебя адрес картинки

картинку лучше с гугла возьми юрлкой

открой картинку в новой вкладке и эту ссыль возьми

Ребят, подскажите пожалуйста, как выполнить функцию, чтобы она прошлась циклом по всем заданным классам, а не закончилась сразу после первого

Квантор всеобщности? Ну... в матане есть. Ну а так стрелочки они везде, знак эквивалентности тоже часто используется.

Неа. Но могу попросить у товарища, если у него есть, скинет. Эту он мне скинул, сказал что ему в своё время очень помогло, сейчас зарабатывает 160 в месяц

Вот если что для JS, может кому пригодится) https://miro.com/app/board/o9J_kxm_io0=/

{ℓ} {A : Set ℓ} ---- я об этом)

Это как раз заморочки Agda, больше из теории типов. А Agda каждый тип это значение некоторого другого типа. Проблема в том, что если описать тип всех типов, который включает сам себя, то возникает парадокс Рассела. Ну или бреет ли брадобрей сам себя? Поэтому все обычные типы (буленовские, натуральные) это значения типа Set 0. Ну а дальше Set 0 это значение типа Set 1, это в свою очередь значение типа Set 2 и так до бесконечности. Ну а тут просто добавлено общности немного, для любого типа любого порядка, ℓ как раз порядок. Ну а Set это не математическое множество, а просто тип типов так назвали

А что такое «логическая математика»?

Хотя лежит у меня учебник по дискретной математике вот думаю учебу закончу и возьмусь))

Как говорится "закончу Х и возьмусь за У" => никогда не случится 😂

Булевую алгебру имел ввиду)

Если говорить точнее, то таблицы истинности высказываний :)

Ребят, помогите. Хочу в фронтэнд, знаю, что нужен js, html и тому подобное, что начать учить первым? Где можно брать тз для практики и наработки опыта?

Ребят, помогите. Хочу в фронтэнд, знаю, что нужен js, html и тому подобное, что начать учить первым? Где можно брать тз для практики и наработки опыта?

тут постоянно кидают, но если хочешь ответ проще, то: html, css, js + framework можешь брать макеты для вёрстки в тг канале, который могу тебе скинуть в лс и делать пет-проекты, могу тоже скинуть в лс

привет всем кто знает почему не установляет pyowm что за ошибка

привет всем кто знает почему не установляет pyowm что за ошибка

pyown и зависимости уже установлены. Предложено обновить pip, но это не ошибка

тут постоянно кидают, но если хочешь ответ проще, то: html, css, js + framework можешь брать макеты для вёрстки в тг канале, который могу тебе скинуть в лс и делать пет-проекты, могу тоже скинуть в лс

Всем привет, ох где вы раньше все были!) за один день просмотра видео от Алексея узнал больше, чем на разных сайтах обучения, но все же есть вопрос, как вы для себя решили какой язык хотите учить?

Всем привет, ох где вы раньше все были!) за один день просмотра видео от Алексея узнал больше, чем на разных сайтах обучения, но все же есть вопрос, как вы для себя решили какой язык хотите учить?

Как канал называется ?

Ты имеешь ввиду ютуб канал где смотрел видео?

привет всем кто знает почему не установляет pyowm что за ошибка