|
Hi Everyone, This is my first time using the forum mailing list. Hope to learn to use it well! If there is a guidance of sort of questions that are appropriate feel free to share it with me, Especially for really basic questions? :) I was trying to do exercise exercise 1.3.1 of https://www.cs.ru.nl/~freek/mizar/mizman.ps.gz 9 easy steps of Mizar. I tried translating phi iff not not phi and put it in mizar and mizar threw me some errors: :: example of a comment
environ
vocabularies MY_MIZAR;
begin
phi implies not not psi & not not psi implies phi;
::>*321
::>
::> 321: Predicate symbol or "is" expected
I put after the environ begin clause but throws an error that isn’t too helpful. How can I check if what I am doing in that exercise I am doing correctly? Regards, Brando |