Телеграмм чат группы rust_offtopic страница 8926

parrot.ru

Рейтинг популярных групп и каналов

В рейтинге участвует:

групп:

каналов:

Виртуальный сервер на SSD - недорого!

Аренда выделенных и виртуальных серверов (VDS/VPS), хостинг, аренда IP-адресов, администрирование, круглосуточная поддержка

qwarta.ru подробнее

Резервное копирование с проверкой на вирусы!!!

Удобный сервис создания резервных копий на любой сервер сети интернет. Отслеживайте изменения, проверяйте на вирусы. Надежно защитите свой бизнес!

go.backupland.com

Выбираете сервер? Любая конфигурация на заказ!

Аренда физических серверов любых конфигураций под любые запросы - 1С бухгалтерия, игровые сервера, нагруженные проекты, интернет-магазины!

qwarta.ru подробнее

Size: a a a

rust_offtopic

360 membersпожаловаться на группу

2020 March 05

AZ

Alex Zhukovsky in rust_offtopic

Вот, простейший пример, обьявление того, что для любого списка xs и любой функции f, такой что для любого элемента x из xs верно f x = x, то map f xs = xs:

map-id₂ : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs
map-id₂ []           = refl
map-id₂ (fx≡x ∷ pxs) = P.cong₂  _∷_  fx≡x (map-id₂ pxs)

Оригинал тут:
https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#2568

как это редактировать через консольные ascii-only редакторы?

источник

14:50пожаловаться #1

T

Tux in rust_offtopic

Ну в идее ^/ — коммент через //, а ^shift+/ — через /**/.

> да и fmt деструктвризует их
Эээм, не должен вообще. У меня он так не делает...

я саблайм использую, очевидно

источник

14:50пожаловаться #2

DS

Doge Shibu in rust_offtopic

как это редактировать через консольные ascii-only редакторы?

Оно через emacs работает, если что, это главный редактор для агды.

источник

14:50пожаловаться #3

Т8

Т-34 85 in rust_offtopic

Оси на этом не пишутся, там чуть хитрее процесс, это все используется для формального доказательства нужных свойств модели.

То есть, для обычного софта оно не нужно?

источник

14:50пожаловаться #4

r

red75prime in rust_offtopic

Roman Proskuryakov

ну да. всем подавай простой С++

Ну да, ведь сложность может быть только одного вида.

источник

14:51пожаловаться #5

AZ

Alex Zhukovsky in rust_offtopic

Оно через emacs работает, если что, это главный редактор для агды.

вот и все, шах и мат

источник

14:51пожаловаться #6

Т8

Т-34 85 in rust_offtopic

Оно через emacs работает, если что, это главный редактор для агды.

А рефакторить это как?

источник

14:51пожаловаться #7

DS

Doge Shibu in rust_offtopic

Т-34 85

То есть, для обычного софта оно не нужно?

Это средства для доказательства свойств, которые являются сами по себе языками программирования.

На них можно писать софт в силу их конструкции, но это не основная их цель. Их цель - это доказательства и их формальная проверка.

источник

14:52пожаловаться #8

T

Tux in rust_offtopic

Вот, простейший пример, обьявление того, что для любого списка xs и любой функции f, такой что для любого элемента x из xs верно f x = x, то map f xs = xs:

map-id₂ : ∀ {f : A → A} {xs} → All (λ x → f x ≡ x) xs → map f xs ≡ xs
map-id₂ []           = refl
map-id₂ (fx≡x ∷ pxs) = P.cong₂  _∷_  fx≡x (map-id₂ pxs)

Оригинал тут:
https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#2568

а что нижний индекс 2 означает?

источник

14:52пожаловаться #9

DS

Doge Shibu in rust_offtopic

а что нижний индекс 2 означает?

Там выше есть чуть другая формулировка, более узкая:

map-id : map id ≗ id {A = List A}
map-id []       = refl
map-id (x ∷ xs) = P.cong (x ∷_) (map-id xs)

Поэтому тут просто индекс 2, как то, что выше была формулировка 1

источник

14:53пожаловаться #10

Т8

Т-34 85 in rust_offtopic

Это средства для доказательства свойств, которые являются сами по себе языками программирования.

На них можно писать софт в силу их конструкции, но это не основная их цель. Их цель - это доказательства и их формальная проверка.

А это не оверкилл?

источник

14:54пожаловаться #11

DF

Dollar Føølish in rust_offtopic

А когда агда успела взлететь ? Обычно же был кок изабель

источник

14:54пожаловаться #12

AZ

Alex Zhukovsky in rust_offtopic

в тчему

источник

14:55пожаловаться #13

DS

Doge Shibu in rust_offtopic

Dollar Føølish

А когда агда успела взлететь ? Обычно же был кок изабель

А я сказал, что она взлетела? Кок и изабель чаще используются и на них реальные проекты делают.

Агду я привел как пример, потому что я её хоть как-то знаю.

источник

14:55пожаловаться #14

DF

Dollar Føølish in rust_offtopic

Ок, не так понял

источник

14:55пожаловаться #15

DS

Doge Shibu in rust_offtopic

Т-34 85

А это не оверкилл?

Смотря для чего.

Выразительность связанную с типами в таких языка, можно очень много где потенциально применить. Делать более выразительные и безопасные библиотеки и т.д.

Именно верификация софта - смотря где. Опять-таки в играх и массовом десктопном софте - пофигу на неё вообще.

В ОСях, серверном софте, всяких смарт-контрактах и финтехе - она вполне может найти свое место.

источник

14:57пожаловаться #16

DS

Doge Shibu in rust_offtopic

Там цена ошибки достаточно велика.

источник

14:57пожаловаться #17

В

Вафель in rust_offtopic

я саблайм использую, очевидно

Уверен что там тоже есть для этого хоткей, я просто его не знаю

источник

14:59пожаловаться #18

T

Tux in rust_offtopic

Уверен что там тоже есть для этого хоткей, я просто его не знаю

Ctrl d же

источник

15:01пожаловаться #19

p

polunin.ai in rust_offtopic

Чуваки, помогите пж
Нужно составить диаграмму использования средства автоматизации автомобильного конвейера
Суть в том, что конвейер полностью автоматизирован, нужно придумать что-то, что может автоматизировать работу связанную с ним.
Вопрос, что можно оптимизировать? Чью работу?

источник

15:06пожаловаться #20