ΑZ
ведите себя хорошо
Size: a a a
2021 May 28
AN
правильно... а почему у меня нету block_on
AN
ладно потом.
AN
давай беги :)
p
Зависит от того как ты хочешь
p
Ты можешь сделать его тьюринг полным
p
А можешь нет
а
Не знаю как в идрисе, но в Coq (f x) = (f x) можно доказать не запуская f
let proof_term : (f x) = (f x) := eq_refl (f x)AS
в смысли? Это же свойство языка? Имеются в виду настройки компилятора?
а
кст в Coq оператор = определён в стандартной библиотеке, а в идрисе это интринзик компилятора
AN
разве, вроде его можно переопределять для списков и для чего хочешь.
AN
а наверное речь была про DecEq
AN
так что я хотел сказать. Для того чтобы не было проблем c IO, получается монаду можно unwrap-нуть только один раз, и это делает рантайм. Тогда мы не можем получить терм в котором будет значение переменной полученной из IO. И нету проблем с конфликтом, что у нас будет у одного выражения разные значения.
AN
то как в пример @Psilon с perform_io() сделано.
/
Кто-нибудь использует vim в качестве замены IDE и сколько нужно времени, чтобы такой редактор не вызывал отвращение?
H
сижу плачу
H
интерфейсы в си)))))
AN
а почему self третьим аргументом?
gо
Потому что первым
gо
тип, название, первый аргумент, второй аргумент...