pikan
commented
10 years ago ╱╱┏╮ ╱╱┃┃ ▉━╯┗━╮ ▉┈┈┈┈┃ ▉╮┈┈┈┃ ╱╰━━━╯ as we discussed! :)
On 8 May 2014 14:33, Steven Obua notifications@github.com wrote:
If variables have no type / set annotation, then it should be allowed to quantify over them without using commas, like so:
∀ x y z. P x y z
Also, when instead of writing
∀ x. ∀ y. ∃ z. ∀ f. P x y (f z)
it should be possible to write
∀ x ∀ y ∃ z ∀ f. P x y (f z)
instead.
— Reply to this email directly or view it on GitHubhttps://github.com/proofpeer/proofpeer-proofscript/issues/5 .
phlegmaticprogrammer
If variables have no type / set annotation, then it should be allowed to quantify over them without using commas, like so:
∀ x y z. P x y z
Also, when instead of writing
∀ x. ∀ y. ∃ z. ∀ f. P x y (f z)
it should be possible to write
∀ x ∀ y ∃ z ∀ f. P x y (f z)
instead.