DM
да, доброе утро, конечно
🥳 спасибо
Size: a a a
2020 January 16
ΛВ
Oℕ
@odomontois надеюсь не сильно побеспокою, но не мог бы ты глянуть пр в дерево?
эх
Oℕ
когда уже эти либы начнут в себя впиливать дерево, а не в дерево всё подряд
ᛒ
Кто такой Нижников?
ᛒ
Какой-то скала разработчик, говорят
http://profyclub.ru/authors/2089
http://profyclub.ru/authors/2089
ᛒ
Тузика, говорят, там порвал
DM
когда уже эти либы начнут в себя впиливать дерево, а не в дерево всё подряд
че т я не подумал об этом
можно было попробовать, все равно добавлял поддержку 2.13 Павкину
можно было попробовать, все равно добавлял поддержку 2.13 Павкину
AT
фиксация же в принципе определяется баиндингом переменной в описании типа?
т.е. если бы сигнатура писалась как
т.е. если бы сигнатура писалась как
Inductive eq (A : Type) (a: A) A : Prop, то последний аргумент никак не определен и его надо указывать в конструкторе, а с переменной он будет фиксирован уже в любом случае (или также Inductive eq (A : Type) : (a : A) -> A -> Prop)Inductive eq A (a : A) (b : A) : Prop зафиксировал бы все компоненты равенства, т.е. мы могли бы написать только eq_refl : eq A a b, что, конечно, лишило бы смысла наше _определение_ равенства.
Ещё можно было бы сделать a индексом:
Inductive eq A : A -> A -> Prop
Это работает, но менее удобно в доказательствах
Ещё можно было бы сделать a индексом:
Inductive eq A : A -> A -> Prop
Это работает, но менее удобно в доказательствах
Oℕ
в ваших грязных доказательствах с аксиомой К
DM
Inductive eq A (a : A) (b : A) : Prop зафиксировал бы все компоненты равенства, т.е. мы могли бы написать только eq_refl : eq A a b, что, конечно, лишило бы смысла наше _определение_ равенства.
Ещё можно было бы сделать a индексом:
Inductive eq A : A -> A -> Prop
Это работает, но менее удобно в доказательствах
Ещё можно было бы сделать a индексом:
Inductive eq A : A -> A -> Prop
Это работает, но менее удобно в доказательствах
это я в лекции видел, да
вопрос чисто синтаксический, можно ли писать паарметры справа от двоеточия и можно ли писать только тип слева
вопрос чисто синтаксический, можно ли писать паарметры справа от двоеточия и можно ли писать только тип слева
AT
в ваших грязных доказательствах с аксиомой К
«Какие ваши доказательства?» (с) Красная жара
Oℕ
это я в лекции видел, да
вопрос чисто синтаксический, можно ли писать паарметры справа от двоеточия и можно ли писать только тип слева
вопрос чисто синтаксический, можно ли писать паарметры справа от двоеточия и можно ли писать только тип слева
и то, и другое можно писать там и там
AT
это я в лекции видел, да
вопрос чисто синтаксический, можно ли писать паарметры справа от двоеточия и можно ли писать только тип слева
вопрос чисто синтаксический, можно ли писать паарметры справа от двоеточия и можно ли писать только тип слева
А, нет, это синтаксисом фиксировано
o
«Какие ваши доказательства?» (с) Красная жара
Кокаинум!
Oℕ
слева - универсальные параметры, справа - индексы
Oℕ
если я правильно понял вопрос
DM
А, нет, это синтаксисом фиксировано
понял, спасибо
AT
Кокаинум!
Эта нэ рука литэйщика