Телеграмм чат группы scala

Size: a a a

ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

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

2020 April 20

Daniel Matveev in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

источник

16:15пожаловаться #1

Oℕ

Oleg ℕizhnik in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

врайт уанс, пуш бинарис, ран эверивере

источник

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

RattenKonig 🍄🌹 in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

эверириване ран

источник

16:18пожаловаться #3

RattenKonig 🍄🌹 in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

с выздоравливанием тебя олег

источник

16:18пожаловаться #4

RattenKonig 🍄🌹 in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

это техно аренд

источник

16:19пожаловаться #5

RattenKonig 🍄🌹 in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

дима

источник

16:19пожаловаться #6

Daniel Matveev in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

все? его забанили за глумление над арендом?

источник

16:19пожаловаться #7

Daniel Matveev in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

я увидел гневный текст, а потом он вдруг пропал

источник

16:20пожаловаться #8

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

ᛒᚨᚱᛏᛟᛋᛋᛟ

как дела

вчера копался с каппой

источник

16:40пожаловаться #9

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

на википедии короч ерунда похоже написана

источник

16:40пожаловаться #10

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

правильная каппа должна выглядеть вот так https://github.com/clayrat/sequent-calc/blob/master/src/Kappa/Term.idr

GitHub

clayrat/sequent-calc

Experiments with sequent calculi. Contribute to clayrat/sequent-calc development by creating an account on GitHub.

источник

16:41пожаловаться #11

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

а не вот это https://en.wikipedia.org/wiki/Kappa_calculus#Typing_rules

Wikipedia

Kappa calculus

In mathematical logic, category theory, and
computer science, kappa calculus is a
formal system for defining first-order
functions.

источник

16:41пожаловаться #12

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

я посмотрел в истории, эту статью один чел в 2011 написал, и с тех пор там только форматирование менялось

источник

16:42пожаловаться #13

RattenKonig 🍄🌹 in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

Alex Gryzlov

правильная каппа должна выглядеть вот так https://github.com/clayrat/sequent-calc/blob/master/src/Kappa/Term.idr

GitHub

clayrat/sequent-calc

Experiments with sequent calculi. Contribute to clayrat/sequent-calc development by creating an account on GitHub.

sticker.webp

(32.36 Кб)

источник

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

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

хз откуда он вытащил эту формулировку, и у Хасегавы, и у Мегача оно выглядит не так

источник

16:42пожаловаться #15

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

ну там ключевое изменение что "Bang" не t |- 1 а t |- t x 1

источник

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

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

иначе не вывести правый изоморфизм и соответственно все сколь-нибудь полезное типа copy/swap

источник

16:45пожаловаться #17

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

и с аксиомой проблемка, в той формулировке подстановка нереализуема

источник

16:46пожаловаться #18

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

вообще интересно что это с логической стороны, и как оно бьется с дедукцией/секвенциями

источник

16:51пожаловаться #19

Alex Gryzlov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)

потому что comp это уже как бы такой cut

источник

16:51пожаловаться #20