Size: a a a

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

2020 January 16

ὦan in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Vasiliy
бля, че они в полный рост стоят
они похоже там 1 челика взяли
источник

ὦan in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Vasiliy
бля, че они в полный рост стоят
источник

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

AT

Anton Trunov in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Daniel Matveev
Inductive eq (A : Type) (a : A) : A -> Prop

Я правильно понял, что отметить конкретный терм (a : A) можно только слева от двоеточия и это в целом особенность синтаксиса coq?
Параметры индуктивного типа имеют область видимости все конструкторы этого типа, становятся параметрами всех конструкторов, кроме того, они фиксированы у всех конструкторов. Т.е. eq_refl : forall A a, eq A a ? - вместо ? можно поставить что угодно (привязав имя и соблюдая типы, конечно), а первые два параметра у eq фиксированы
источник

DM

Daniel Matveev in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
фиксация же в принципе определяется баиндингом переменной в описании типа?

т.е. если бы сигнатура писалась как Inductive eq (A : Type) (a: A) A : Prop, то последний аргумент никак не определен и его надо указывать в конструкторе, а с переменной он будет фиксирован уже в любом случае (или также Inductive eq (A : Type) : (a : A) -> A -> Prop)
источник

DM

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

что несколько фиксирует порядок в сигнатурах
источник

KS

Kirill Shelopugin in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
LUL Лостфильм наконец-то заблокировали
источник

KS

Kirill Shelopugin in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
А я все думал какого хуя они медлят
источник

V

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

KS

Kirill Shelopugin in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Не скажу
источник

V

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

I

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

KS

Kirill Shelopugin in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Разве на лостфильме есть субтитры? Вообще мы смотрим с женой, а ей лень напрягаться смотреть на ангельском, так что смотрим на русском
источник

V

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

ὦan in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Vλadimir
А что смотрите то
источник

V

Vλadimir in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Зачем ты везде лезешь
источник

KS

Kirill Shelopugin in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Вовка не очень хорошо читает, только хорошо на баше пишет
источник

ὦan in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Vλadimir
Зачем ты везде лезешь
Я тебе помогаю найти ответы
источник

ὦan in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
А ты мне грубишь
источник

ὦan in ПОКА ОДЕРСКИ НЕ ВИДИТ (как мы разрешаем котикам срать)
Вот что за люди
источник