Первый пример Изабель - PullRequest
Новая
       16

Первый пример Изабель

1 голос
/ 05 октября 2019

Я пытался воспроизвести короткий пример из третьего урока Мохамеда Абуэльвафа на YouTube, но не смог обойти ошибку синтаксического анализа. Мохамед показывает, как ввести двойную стрелку вправо как ==, но это не работает на моей Изабель 2019, поэтому я использовал Symbols / Arrow, чтобы получить ее. Кроме этого я не могу думать ни о чем, но все еще не могу заставить это работать. Что бы я ни пытался, это не разбирается. Помогите кому-нибудь? Спасибо! 

theory example
imports FOL
begin

lemma ex1: "⟦ A; B ⟧ ⟹  A ⋀ B" 
  apply (rule conjI)
  apply assumption
  apply assumption
  done

end

1 Ответ

2 голосов
/ 06 октября 2019

Когда я скопировал ваш код в Изабель, я обнаружил что-то вроде опечатки: «A ⋀ B», а не «A ∧ B»

Они выглядят очень похоже на StackOverflow, но в первой Изабельнамного больше и не является правильным символом для использования.

Когда я изменил его на последний символ, error, ошибка синтаксического анализа исчезла, и доказательство успешно завершено. Если вы начнете набирать \and, это позволит вам выбрать правильный символ из выпадающего меню.

Надеюсь, это поможет:)

...