В
можно, так и делаю, это дело потом отревьюю, спасибо)
Запусти потом клиппи, много чего интересного можно найти
Size: a a a
2020 March 05
T
/**/ в помощь, для этого обычно хоккей есть. И зачем тебе комментировать импорты?
Ctrl + d, и он комментит именно через //
да и fmt деструктвризует их
да и fmt деструктвризует их
Т8
Какая-нибудь низкоуровневая штука верифицированная, тот же менеджер памяти или рантайм асинхронный
Мы говорим про твой код
T
Запусти потом клиппи, много чего интересного можно найти
у меня в пайплайне он есть и да, ругается, но это всё после основного процесса разработки модуля
G
Т-34 85
Мы говорим про твой код
смотри сообщение ниже
DS
Т-34 85
Хотел бы посмотреть
Вот, простейший пример, обьявление того, что для любого списка xs и любой функции f, такой что для любого элемента x из xs верно f x = x, то map f xs = xs:
Оригинал тут:
https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#2568
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
Т8
Два проекта от одной и той же команды. Так, а ещё что?
RP
Т-34 85
Два проекта от одной и той же команды. Так, а ещё что?
Т8
вернее проект 6+ разработчиков
Они делают то, что у тебя не получается?
G
Т-34 85
Они делают то, что у тебя не получается?
хз, все получается
G
можешь посмотреть по коммитам
Т8
То есть, всё так не густо, что надо вести список?
В
Ctrl + d, и он комментит именно через //
да и fmt деструктвризует их
да и fmt деструктвризует их
Ну в идее
> да и fmt деструктвризует их
Эээм, не должен вообще. У меня он так не делает...
^/ — коммент через //, а ^shift+/ — через /**/.> да и fmt деструктвризует их
Эээм, не должен вообще. У меня он так не делает...
Т8
Вот, простейший пример, обьявление того, что для любого списка xs и любой функции f, такой что для любого элемента x из xs верно f x = x, то map f xs = xs:
Оригинал тут:
https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#2568
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
Я теперь понимаю, почему вряд ли ОС будут на этом написаны. Пушто писать некому
RP
ну да. всем подавай простой С++
Т8
можешь посмотреть по коммитам
Ладно, гляну быстро, если оно гуглится
Т8
ну да. всем подавай простой С++
Ващет, да
DS
Т-34 85
Я теперь понимаю, почему вряд ли ОС будут на этом написаны. Пушто писать некому
Оси на этом не пишутся, там чуть хитрее процесс, это все используется для формального доказательства нужных свойств модели.