Skip to content
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.

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

Introduce separate Prop type #186

Closed
byorgey opened this issue Jun 3, 2020 · 1 comment · Fixed by #217
Closed

Introduce separate Prop type #186

byorgey opened this issue Jun 3, 2020 · 1 comment · Fixed by #217

Comments

@byorgey
Copy link
Member

byorgey commented Jun 3, 2020

Bool is a subtype of Prop. Things like forall, exists create a Prop.
Things like and, or can work with both. A Prop can be
evaluated into a Bool, using a built-in primitive named something like eval, or check, (this might not terminate), or tested using a primitive like test (which terminates). Maybe test returns some special algebraic type representing possible outcomes (definitely false (with counterexample?); definitely true; probably true; probably false).

@byorgey byorgey added the C-Project A larger project that may take multiple days. label Jun 4, 2020
byorgey added a commit that referenced this issue Jun 4, 2020
@byorgey
Copy link
Member Author

byorgey commented Jun 4, 2020

  • Add Prop as a supertype of Bool
  • Make and, or, not, implies polymorphic
  • Make special assertion operators like ==!, <!, etc. which can only make a Prop and have special behavior when reporting test failures?
  • Add eval prim to turn Prop into Bool
  • Add forall and exists expression forms
  • Add test primitive
  • get rid of Property as a separate thing

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant