Simpler version: always use ==>
Only exception: when you work under \forall
Alex Weisberger has marked this topic as resolved.
Mathias Fleury said:
Only exception: when you work under \forall
But then, when do you work under ∀? You can and usually should use ⋀ instead. You have to use ⟶ and ∀ only where you have to use bool
, which typically is in a definition.
What about expressing this as:
theorem "⟦beval1 t t'; beval1 t t''⟧ ⟹ t' = t''"
This seems to work as well, and for me is a little more clear because the premises are clearly grouped together.
Wolfgang Jeltsch said:
You have to use ⟶ and ∀ only where you have to usebool
, which typically is in a definition.
This is what i meant with \forall…
Wolfgang Jeltsch said:
But then, when do you work under ∀? You can and usually should use ⋀ instead.
I don't agree: all tactics and compositon work on ==>
and !!
(induction, rule, OF, of, ...). Hence the default choice for theorems should always be the Pure symbols
Mathias Fleury said:
Wolfgang Jeltsch said:
But then, when do you work under ∀? You can and usually should use ⋀ instead.I don't agree: all tactics and compositon work on
==>
and!!
(induction, rule, OF, of, ...). Hence the default choice for theorems should always be the Pure symbols
Isn’t this what I said above? :wink:
ah sorry I misunderstood you then…
I thought that your You can and usually should use ⋀ instead
was meant in general, and not only below ∀
Mathias Fleury said:
I thought that your
You can and usually should use ⋀ instead
was meant in general, and not only below ∀
Of course, it was meant in general, and that’s what you’re saying as well, right? I mean, ⋀
is the same as !!
, a pure symbol, and you’re saying, “Hence the default choice for theorems should always be the Pure symbols”.
I find ‹⋀∧› and ⋀∧
too hard to distinguish
Last updated: Oct 12 2024 at 20:18 UTC