AA
наоборот
Size: a a a
2020 May 23
DF
Спасибо!
Oℕ
Dollar Føølish
А как это подгуглить? Discipline stack?
isA64Msacrastic : (c : Comment A64m_qb0) -> Dec (Sarcastic c)
isA64Msacrastic c = Yes (a64mAlwaysSarcastic c)
isA64Msacrastic c = Yes (a64mAlwaysSarcastic c)
R
isA64Msacrastic : (c : Comment A64m_qb0) -> Dec (Sarcastic c)
isA64Msacrastic c = Yes (a64mAlwaysSarcastic c)
isA64Msacrastic c = Yes (a64mAlwaysSarcastic c)
конструктивненько
AA
все еще не вижу ответа
AA
Переслано от A64m AL256m qn<co...
а наоборот, из идрисострадальцев кто-нибудь агду прилично знает?
R
Переслано от A64m AL256m qn<cores> I0
а наоборот, из идрисострадальцев кто-нибудь агду прилично знает?
существенная часть агдострадальцев не знают агду прилично, так что я сомневаюсь
R
хотя может и найдется кто-то
Oℕ
Переслано от A64m AL256m qn<cores> I0
а наоборот, из идрисострадальцев кто-нибудь агду прилично знает?
Ну очевидно, что пока что ни одного такого, если они есть, этот вопрос не увидело
R
существенная часть агдострадальцев не знают агду прилично, так что я сомневаюсь
из-за того, что доки куцые, приходится все реверс-инжинирить
AA
Ну очевидно, что пока что ни одного такого, если они есть, этот вопрос не увидело
можно написать не про собственный опыт!
Oℕ
still no
Oℕ
Возможно, есть страдальцы, которые пытались, но по ряду причин сочли агду ещё хуже чем агдострадальцы идрис
Oℕ
Oℕ
Переслано от Alex Gryzlov
в каждом проекте с нуля определять, начиная с булей
R
ну у агды есть стдлиб
AA
удивительно, завтипострадалец испугался ручного труда
R
но реально дешевле себе самому все определить, учитывая как часто они ломают обратную совместимость
R
впрочем у агды есть и другая стдлиб. С ней может получше это все
Oℕ
удивительно, завтипострадалец испугался ручного труда
Когда уже завтипный хаскель вмержат, чтобы можно было над ним издеваться