DB
ну просто вот так
Да у них же даже длина разная
Size: a a a
2020 December 04
DB
Такова не бывает
к
ну смотри
AG
тут равенство ослабленное
DB
В смысле! Кем!
к
data nat = zero | succ nat
data int where
pos : nat -> int
neg : nat -> int
neg_zero_eq_zero : pos zero = neg zero
получается тип, где pos zero доказуемо равно neg zero, хоть конструкторы разные
и доказательство это как раз наш конструктор neg_zero_eq_zero
data int where
pos : nat -> int
neg : nat -> int
neg_zero_eq_zero : pos zero = neg zero
получается тип, где pos zero доказуемо равно neg zero, хоть конструкторы разные
и доказательство это как раз наш конструктор neg_zero_eq_zero
к
конструкторы это же аксиомы
AG
В смысле! Кем!
создателями теории :)
DB
data nat = zero | succ nat
data int where
pos : nat -> int
neg : nat -> int
neg_zero_eq_zero : pos zero = neg zero
получается тип, где pos zero доказуемо равно neg zero, хоть конструкторы разные
и доказательство это как раз наш конструктор neg_zero_eq_zero
data int where
pos : nat -> int
neg : nat -> int
neg_zero_eq_zero : pos zero = neg zero
получается тип, где pos zero доказуемо равно neg zero, хоть конструкторы разные
и доказательство это как раз наш конструктор neg_zero_eq_zero
Вместо равно стрелка?
к
нет
AG
не, в том то и фишка
DB
Капец
AG
это так называемый высший индуктивный тип
AG
который позволяет натягивать мосты между конструкторами
DB
Неясно. А что мы построим-то этим конструктором
к
если посмотреть на теорию групп и на фактор-группы, то может появится некоторая интуиция
к
Неясно. А что мы построим-то этим конструктором
пруф равенства
DB
если посмотреть на теорию групп и на фактор-группы, то может появится некоторая интуиция
Боюсь стать шизоидом, как Михайлов
DB
пруф равенства
То есть он возвращает не int?
NI
Боюсь стать шизоидом, как Михайлов
Ой вей. Всего-то фактор-группы...