diff options
| author | Matthew Sotoudeh <matthew@masot.net> | 2023-01-04 23:01:35 -0800 |
|---|---|---|
| committer | Matthew Sotoudeh <matthew@masot.net> | 2023-01-04 23:01:35 -0800 |
| commit | abcb1bcd4dca20e0019e4e3c599b92ea81b0589d (patch) | |
| tree | 1ee6d3d115ee4fa0c54e6792f4c08786813d34b5 | |
| parent | 8a4d48b1b832d8a00dea739dcc41fb1ca5d21cbc (diff) | |
indicate pseudo-claims
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | examples/group.z3fc | 4 | ||||
| -rw-r--r-- | examples/readme.z3fc | 2 |
3 files changed, 4 insertions, 4 deletions
@@ -168,7 +168,7 @@ Similarly, finite sets can be constructed on-the-fly with finite set notation: [check fin sets] forall x. forall y. forall z. (z in {x, y}) iff ((z = x) or (z = y)) - by [Taut], {FinSet}; + by {Taut}, {FinSet}; ``` where here the `{x, y}` is replaced at parse-time with `_fin_set_2(x, y)` and the `{FinSet}` pseudo-claim adds essentially the `[check fin sets]` assumption diff --git a/examples/group.z3fc b/examples/group.z3fc index 6866cf7..cfa44ea 100644 --- a/examples/group.z3fc +++ b/examples/group.z3fc @@ -43,9 +43,9 @@ take xinv s.t. [L4] ((x + y) = (x + z)) implies (y = z) - by [Implication], [L3], [L1]; + by {Implication}, [L3], [L1]; [left cancellation (manually)] forall x. forall y. forall z. ((x + y) = (x + z)) implies (y = z) - by [Generalize], [L4]; + by {Generalize}, [L4]; diff --git a/examples/readme.z3fc b/examples/readme.z3fc index ee6a481..ae6d89e 100644 --- a/examples/readme.z3fc +++ b/examples/readme.z3fc @@ -68,4 +68,4 @@ by [0 in Naturals], [0 < 1], {FilterSet}; [check fin sets] forall x. forall y. forall z. (z in {x, y}) iff ((z = x) or (z = y)) -by [Taut], {FinSet}; +by {Taut}, {FinSet}; |