Skip to content

Update sidenote-quantifiers.html #70

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
hardroadcrush wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Update sidenote-quantifiers.html #70

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c1a393a
Update sidenote-quantifiers.html
hardroadcrush Mar 31, 2026
c4e18ea
Update sidenote-quantifiers.html
hardroadcrush Apr 2, 2026
d0bd67c
Update sidenote-quantifiers.html
hardroadcrush Apr 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 6 additions & 16 deletions tutorials/online/sidenote-quantifiers.html
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
<body>
<h2>Quantifiers</h2>

<p> The Alloy quantifiers are </p>
<p> The Alloy quantifiers are : <i>all</i>, <i>some</i> , <i>no</i>, <i>one</i>, <i>lone</i>. </p>
<ul>
<li> <tt><b> all x:X | formula </b></tt> - every <b><tt>x</b></tt> of type
<b><tt>X</b></tt> satisfies <b><tt>formula</b></tt>. If there are
Expand All @@ -28,27 +28,17 @@ <h2>Quantifiers</h2>

<p> Note that a 'formula' is something that evaluates to a boolean
value, as opposed to an 'expression' which evaluates to a
(relational) value. With "some", "no", one", and "lone", you can also apply

@pkriens pkriens Apr 1, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why did you remove this?

@hardroadcrush hardroadcrush Apr 2, 2026

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Redundant. Does not provide much clarity either since we dont know where exactly it can be used.
It cannot be used anywhere sets or relations are mentioned right.
So I left the exact usage arbitary but mentioned that it can be done.

them to a set or a relation like this:</p>

<ul>
<li> <tt><b> some X </b></tt> - there is at least one
<b><tt>X</b></tt></li>
<li> <tt><b> no X </b></tt> - there are no <b><tt>X</b></tt>'s</li>
<li> <tt><b> one X </b></tt> - there is exactly one <b><tt>X</b></tt></li>
<li> <tt><b> lone X </b></tt> - there are either zero or one
<b><tt>X</b></tt>'s</li>
</ul>

(relational) value. The quantifiers "some", "no", one", and "lone", can also
be applied to a set or a relation.
<hr WIDTH="100%">

<p> The basic format for a quantifier is</p>
<p> The usual format for using a quantifier is:</p>

<b><pre>
quantifier variable:type | formula
</b></pre>

<p> where the formula may includes references to the quantifier
<p> where the formula may include references to the quantifier
variable. An alternative notation is:</p>

<b><pre>
Expand All @@ -73,7 +63,7 @@ <h2>Quantifiers</h2>
arbitrarily complex formulas.</p>

<p> However, be warned that nested quantifiers may cause your model to
become intractable. In generaly, try not to stack more than two
become intractable. In general, try not to stack more than two
or three of them together.</p>

</body>
Expand Down