Публикации по теме 'lean'
Переключатели функций сборки для Nuxt.js
Переключатели функций - это мощная утилита в современном мире, особенно для команд, которые ежедневно развертывают множество функций. А когда вы соедините это с мощным фреймворком, таким как Nuxt.js, вы действительно разовьете возможности для быстрого перемещения и сохранения высокого уровня качества кода.
Так что же такое переключение функций? 🤔
Переключение функции - это простое условие, которое контролируется с помощью внешней или локальной конфигурации, чтобы определить, видит..
Вопросы по теме 'lean'
Почему и класс типов, и механизм неявных аргументов?
Таким образом, у нас могут быть явные аргументы, обозначаемые () . Мы также можем иметь неявные аргументы, обозначаемые {} .
Все идет нормально.
Однако зачем нам также нужна [] нотация конкретно для классов типов?
В чем разница между...
57 просмотров
schedule
20.10.2021
Как упростить доказательство индукцией в Lean?
Я хотел бы упростить доказательство индукцией по бережливому производству.
Я определил индуктивный тип с 3 конструкторами в Lean и бинарным отношением для этого типа. Я включил аксиомы, потому что Lean не позволил бы мне использовать их в качестве...
352 просмотров
schedule
08.03.2022
Как доказать формулы математической индукции в программе доказательства теорем LEAN?
Может ли кто-нибудь помочь мне понять, как написать доказательство простого результата, который можно легко получить с помощью индукции, например формулы для суммы первых n натуральных чисел: 1+2+...+n = n(n+1)/2 , используя средство доказательства...
336 просмотров
schedule
22.04.2022
Определение выбора в Lean
В Lean «выбор» реализован в соответствии с:
Наша аксиома выбора теперь выражается просто следующим образом:
axiom choice {α : Sort u} : nonempty α → α
Учитывая только утверждение h, что α непусто, выбор h волшебным образом дает элемент...
243 просмотров
schedule
20.09.2023
Как доказать пример в Lean?
Ниже представлена моя неправильная попытка. Есть предложения о том, как действовать?
def le(f g : ℕ) : Prop := ∃ a : ℕ , a + f = g
local notation a ≤ b := le a b
example : ∀ f g : ℕ , f ≤ g → g ≤ f → f = g :=
begin
assume f g fg...
80 просмотров
schedule
07.11.2022
Бережливое определение групп
Это дополнительный вопрос о типе прохода в качестве параметра
Я попробовал предложение jmc, которое, похоже, сработало, но потом я застрял в другом месте. Первоначальная цель вопроса состояла в том, чтобы определить категории групп и колец, но...
41 просмотров
schedule
04.08.2023
Не могу заставить классы шрифтов работать в Lean
У меня возникли проблемы с пониманием того, как инициировать использование классов типов Lean. Вот попытка небольшого примера:
section the_section
structure toto [class] (A : Type) := (rel : A → A → Prop) (Hall : ∀ a, rel a a)
definition P A :=...
72 просмотров
schedule
16.10.2023
Что делает натуральные числа такими особенными в отношении тайм-аута?
В предыдущем вопросе о формализации подмножеств евклидовых пространств я получил следующий ответ о том, как создать n-мерное евклидово пространство :
def euclidean_space (n : ℕ) : Type := set (repeated_prod n ℝ)
И я получил следующий ответ...
65 просмотров
schedule
24.02.2024
