История изменений

(length xs < length ys) – не тип. Разве так можно?

Я сейчас до путя не помню как именно в идрисе, но в целом это работает так: есть два варианта <, один для типов и второй булевский. В коке те которые для типов обозначаются <, <=, >, >= (или соотвественно lt, le, gt, ge), а те которые булевские - <?, <=?, >?, >=? (ltb, leb, gtb, geb). В идрисе точно не помню, но там так же. Нужен соответсвенно тот который для типов. (Т.е. тот который булевский - принимает два натуральных числа, а возвращает булевское значение, а тот который для типов - принимает два натуральныч числа, а возвращает тип).

(length xs < length ys) – не тип. Разве так можно?

Я сейчас до путя не помню как именно в идрисе, но в целом это работает так: есть два варианта <, один для типов и второй булевский. В коке те которые для типов обозначаются <, <=, >, >= (или соотвественно lt, le, gt, ge), а те которые булевские - <?, <=?, >?, >=? (ltb, leb, gtb, geb). В идрисе точно не помню, но там так же. Нужен соответсвенно тот который для типов. (Т.е. тот который булевский - принимает натуральное число, возвращает бул, а тот который для типов - принимает натуральное число, возвращает тип).

(length xs < length ys) – не тип. Разве так можно?

Я сейчас до путя не помню как именно в идрисе, но в целом это работает так: есть два варианта <, один для типов и второй булевский. В коке те которые для типов обозначаются <, <=, >, >= (или соотвественно lt, le, gt, ge), а те которые булевские - <?, <=?, >?, >=? (ltb, leb, gtb, geb). В идрисе точно не помню, но там так же. Нужен соответсвенно тот который для типов. (Т.е. тот который булевский - принимает натуральное число, возвращает бул, а тот который для типов - принимает натуральное число, возвращает утверждение).

(length xs < length ys) – не тип. Разве так можно?

Я сейчас до путя не помню как именно в идрисе, но в целом это работает так: есть два варианта <, один для типов и второй булевский. В коке те которые для типов обозначаются <, <=, >, >= (или соотвественно lt, le, gt, ge), а те которые булевские - <?, <=?, >?, >=? (ltb, leb, gtb, geb). В идрисе точно не помню, но там так же. Нужен соответсвенно тот который для типов. (Т.е. тот который булевский - принимает нат, возвращает бул, а тот который для типов - принимает нат, возвращает утверждение).

(length xs < length ys) – не тип. Разве так можно?

Я сейчас до путя не помню как именно в идрисе, но в целом это работает так: есть два варианта <, один для типов и второй булевский. В коке те которые для типов обозначаются <, <=, >, >= (или соотвественно lt, le, gt, ge), а те которые булевские - <?, <=?, >?, >=? (ltb, leb, gtb, geb). В идрисе точно не помню, но там так же. Нужен соответсвенно тот который для типов.