AZ
компилятор там 1 кнопкой ставится и есть подсветка для вскод, попробовал бы хоть
Size: a a a
2020 August 08
AZ
а то так и будешь думать что скобки это топ
Т8
ну да, такое бывает нужно
Или хотя бы статическую рефлексию как в D
AZ
Т-34 85
Или хотя бы статическую рефлексию как в D
ну идрис на порядок круче. Типы там такие же значения, а значения - такие же типы. Например
let x = Int
let y : x = 10Т8
ну идрис на порядок круче. Типы там такие же значения, а значения - такие же типы. Например
let x = Int
let y : x = 10Беда в том, что идрис - ресёрч язык
AZ
то есть во-первых тип можно сохранить в переменную, во-вторых его можно использовать. На плюсах было бы что-то типа
auto x = int;
x y = 10;Т8
Правда, ди не далеко ушёл
AZ
Т-34 85
Беда в том, что идрис - ресёрч язык
во-первых часть навыков переносится на любой яп, а во-вторых что вчера было ресерчем завтра уже во всех магазинах страны
AZ
ну и просто знать чуть больше вроде не грех
p
только b это не тип, это значение типа Bool
Тип
p
во-первых часть навыков переносится на любой яп, а во-вторых что вчера было ресерчем завтра уже во всех магазинах страны
Завтра - через 30 лет, а так все правильно😄
AZ
Тип
тип это значение типа Type, а Bool - это не Type
p
тип это значение типа Type, а Bool - это не Type
Bool не Type, ты себя слышишь?
p
Bool как раз имеет тип Type
AZ
Bool не Type, ты себя слышишь?
ты меня не читаешь, я говорю что
b : Bool - значит что b значение типа Bool (то есть просто "значение")
А вот было бы
b : Type - тогда был бы ты прав
b : Bool - значит что b значение типа Bool (то есть просто "значение")
А вот было бы
b : Type - тогда был бы ты прав
AZ
типы которые зависят от типов и в расте есть - это просто экзистенциалы или генерики (в зависимости от \forall \exists)
AZ
ну и возможно так проще:
if работает со знаениями а не с типами. if blabla проверяет условие, а не какие-то там типыp
Ладно, мне просто нравится когда ты что-то доказываешь😁
p
Ну и правильнее будет сказать что тип зависит от терма а не от значения
p
ну идрис на порядок круче. Типы там такие же значения, а значения - такие же типы. Например
let x = Int
let y : x = 10Мне тут затирали люди с 16 лет опыта работы в хайлоаде что дженерики не нужны, а ты со своим идрисом😂