diff options
author | Matthew Sotoudeh <matthew@masot.net> | 2023-01-04 23:13:47 -0800 |
---|---|---|
committer | Matthew Sotoudeh <matthew@masot.net> | 2023-01-04 23:13:47 -0800 |
commit | fa165998447d5a9c428eeb614bd703b4031053d1 (patch) | |
tree | 6bfb4cf41ea488af25bfdf7f661195334dab2f12 | |
parent | abcb1bcd4dca20e0019e4e3c599b92ea81b0589d (diff) |
-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}; |