DB
Ой вей. Всего-то фактор-группы...
Кто его знает, что будет дальше
Size: a a a
2020 December 04
AG
все списки подобного типа стягиваемы в точку
к
То есть он возвращает не int?
он возвращает пруф равенства
а равенство элементов типа X это функция от [0..1] -> X
то есть для a, b : X
p : a = b
это функция [0..1] -> X где
p 0 = a
p 1 = b
и p при этом является неприрывной
вот этот конструктор задает аксиому что между neg 0 и pos 0 существует неприрывный путь
а равенство элементов типа X это функция от [0..1] -> X
то есть для a, b : X
p : a = b
это функция [0..1] -> X где
p 0 = a
p 1 = b
и p при этом является неприрывной
вот этот конструктор задает аксиому что между neg 0 и pos 0 существует неприрывный путь
DB
Хорошо, как тогда расшифровать
forall x e -> x :: e = e?
forall x e -> x :: e = e?
к
Хорошо, как тогда расшифровать
forall x e -> x :: e = e?
forall x e -> x :: e = e?
для любого x и e, список x :: e равен e)
AG
это доп ограничение на тип
AG
т.е. когда ты будешь что-то с термом этого типа делать, тебя язык заставит соблюдать это условие
DB
т.е. когда ты будешь что-то с термом этого типа делать, тебя язык заставит соблюдать это условие
Понятно, шо ограничение. Пока не доходит его суть. Ща дайте переварить..
AG
да тут нет особой сути, это гийом от балды написал побаловаться
AG
ща найду поосмысленнее пример
к
с int мне кажется пример поосмысленнее
к
ну в том смысле что его проще осмыслить
к
)
AG
вот например OddList
AG
список где неважен порядок элементов
DB
Ага, вот тут понятно что такое ослабленные равенство
DB
И его я даже понял
DB
А вот про равенство списка и его хвоста это что-то шизоидное, страшное