X
ну насколько я понял, Coq выйдет с очень большим бойлерплейтом. Я могу ошибаться, руками его пока не тыкал
Size: a a a
2021 July 15
X
ты второй, кто советует lean. Над попробовать.
X
а, не, вру. Третий.
X
точно надо, third's the charm
A
Да, там вроде всё красиво получается и автоматика хорошая, хотя сам тоже не пробовал пока
X
аааааааа
X
вспомнил, кто-то мне говорил, что в Lean есть наследование типов-записей
X
надеюсь, не соврал
X
интересно, там есть вещь типа F* type refinements?
X
типа
type even = x:int{ (x % 2) = 0 }a
конечно нет, эти пруверы еще очень далеко от непримитивных доказательств
2021 July 17
TA
Вопрос возможно глупый,но есть ли какой-то способ построить на основе любого бесконечного множестве какое-то поле?
Т.е. дано какое-то множество,а на нем строятся операции сложения и умножения со свойствами поля.
Т.е. дано какое-то множество,а на нем строятся операции сложения и умножения со свойствами поля.
X
если в изначальном кольце нет делителей нуля, то конструкция называется "поле частных"
X
если речь именно про определение операций так, чтобы они над данным множеством образовали поле — ну, строй биекцию этого бесконечного множества на Q или C, и мапь операции из этих полей
TA
А если множество по мощности больше C?
lg
Поля бывают сколь угодно большие, можно добавлять формальные переменные t_s, где s индексируются любым множеством
CD
если я правильно понимаю автора, вопрос: верно ли, что любое бесконечное множество может быть множеством элементов поля
lg
Для этого достаточно понять, что поля бывают сколь угодное большие, а дальше выбрать какую-то биекцию между нашим множеством и каким-то полем такой же мощности и насильно ввести операции на множестве с помощью этой биекции
TA
Я не совсем понял,какими будут элементы такого поля.
A
Берёшь любое поле и трансцендентно расширяешь