Skip to content

Commit

Permalink
Merge pull request #1521 from AmpersandTarski/RieksJ-patch-1
Browse files Browse the repository at this point in the history
Added some explanations to `ENFORCE` statement
  • Loading branch information
hanjoosten authored Oct 29, 2024
2 parents 784c48f + 8e1a988 commit ccebce8
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion docs/reference-material/syntax-of-ampersand.md
Original file line number Diff line number Diff line change
Expand Up @@ -545,7 +545,7 @@ ENFORCE <RelationRef> <type>?
<Term>
```

The `<operator>` can be one of **`:=`,** `:<` or `>:` .
The `<operator>` can be one of **`:=`**, `:<`, or `>:` .

This statement may occur anywhere within a context, either inside or outside a pattern.

Expand All @@ -561,6 +561,8 @@ ENFORCE r := s;t
of the term s;t . It will do so by changing the contents of r
without affecting the contents of s;t .
The effect can be observed in the prototype.
This statement ensures that the rule `r = s;t` is continuously enforced.
(by populating or depopulating `r`, as necessary).
-}
```

Expand All @@ -573,6 +575,8 @@ ENFORCE canDrive :< hasCar /\ hasDriverLicence
So, whenever a person can drive, that person needs to have a car and a driver licence.
However, if that person has both these assets, it is still possible that he/she
cannot drive.
This statement ensures that the rule `canDrive |- hasCar /\ hasDriverLicense` is continuously enforced
(only by depopulating `canDrive` whenever necessary).
-}
```

Expand Down

0 comments on commit ccebce8

Please sign in to comment.