lean

1зной

1ответ

Невозможно заставить классы классов работать в Lean

У меня возникли проблемы с пониманием того, как запускать использование классов типов Lean. Вот попытка небольшой пример: section the_section structure toto [class] (A : Type) := (rel : A → A → Prop)

1зной

2ответ

Индуктивный тип, построенный по списку этого типа в Lean

Я хотел бы определить индуктивный тип, который может быть построен из списка самого себя в постном. Однако inductive a : Type := | aFromAs : list a → a выдает ошибку: failed to infer inductive data

1зной

1ответ

Использование получить в тактическом режиме в Lean теорема расстойки

Как использовать гипотезу о форме H : exists x, P x в тактическом режиме? В перспективе режиме Я хотел бы использовать obtain x Hx, from H,

1зной

2ответ

Как определить частично упорядоченные множества в Lean?

Я хочу доказать this theorem в теореме Lean. Во-первых, мне нужно определить такие вещи, как частично упорядоченные множества, чтобы я мог определить infimum/supremum. Как это делается в Lean? The tut

5зной

1ответ

Как определить взаимные индуктивные предложения в Lean?

Я пытаюсь использовать синтаксис для индуктивных типов данных, но получил сообщение об ошибке «взаимно индуктивные типы должны компилироваться в базовый индуктивный тип с зависимым устранением». Ниже

2зной

1ответ

Почему Lean применяет аргументы рекурсивного типа для отображения после нерекурсивных?

следующее определение отвергается Lean: inductive natlist | nil : natlist | cons: natlist → ℕ → natlist с сообщением об ошибке "ARG # 2 из 'natlist.cons' не является рекурсивной, но это происходит

2зной

1ответ

Идемпотенты коммутативного кольца в помощнике по проверке на лету

Привет, я пытаюсь сделать некоторую математику в помощнике Lean proof, чтобы посмотреть, как это работает. Я решил, что должно быть весело играть с идемпотентами коммутативного кольца. Вот что я пробо