diff options
| -rw-r--r-- | README.md | 7 | ||||
| -rw-r--r-- | examples/readme.z3fc | 2 |
2 files changed, 7 insertions, 2 deletions
@@ -149,7 +149,7 @@ notation of the form `{x in BigSet | P(x)}`: take Naturals; take 0 s.t. [0 in Naturals] 0 in Naturals; take 1 s.t. [0 < 1] 0 < 1; -[negatives are less than 1] +[zero in less-than-one] 0 in {x in Naturals | x < 1} by [0 in Naturals], [0 < 1], {FilterSet}; ``` @@ -162,6 +162,11 @@ forall a. iff ((x in Naturals) and x < a) ``` +It is not expected that users add many more axiom schemata to the system. +Instead, it is expected that most other axiom schemas one might want to use can +be modified to just take a set, then use filtering to achieve the desired goal. +For example, the induction schema of Peano arithmetic can easily be rewritten +to define inductive subsets of the naturals, rather than inductive predicates. Similarly, finite sets can be constructed on-the-fly with finite set notation: ``` diff --git a/examples/readme.z3fc b/examples/readme.z3fc index ae6d89e..cd5a156 100644 --- a/examples/readme.z3fc +++ b/examples/readme.z3fc @@ -61,7 +61,7 @@ take Naturals; take 0 s.t. [0 in Naturals] 0 in Naturals; take 1 s.t. [0 < 1] 0 < 1; -[negatives are less than 1] +[zero in less-than-one] 0 in {x in Naturals | x < 1} by [0 in Naturals], [0 < 1], {FilterSet}; |