Conversation
This doesn't yet pipe the new constructs through the typechecker.
Hook them up through the typechecker. However, we still need implementations.
We define `inf /^ n = inf` and `inf %^ n` for finite, positive `n`.
|
Documentation updates are still needed, but I wanted to make sure we are happy with the syntax choices before doing that. |
Minor output changes in the exercises are required.
|
@robdockins the notation makes sense to me. The only improvement I can think of is to clarify in the comment-docs for the "inclusive" constructs (the non |
We need to avoid the new `down` keyword.
yav
left a comment
yav
left a comment
There was a problem hiding this comment.
I think there are a few more changes that we need for the solver, to match the more relaxed constraints on /^ and /%.
Otherwise it looks good to me, with the caveat that I didn't go over the evaluation semantics in detail
|
AFAICT, the remaining failures are not related to this PR. |
|
@yav, @brianhuffman, any additional thoughts about this? |
Add stub implementations of the new enumeration primitives from GaloisInc/cryptol#1227, and fix up the type of `ecFromTo`, which also changed slightly in that PR.
Add stub implementations of the new enumeration primitives from GaloisInc/cryptol#1227, and fix up the type of `ecFromTo`, which also changed slightly in that PR.
Add stub implementations of the new enumeration primitives from GaloisInc/cryptol#1227, and fix up the type of `ecFromTo`, which also changed slightly in that PR.
2 participants
This PR adds new syntactic forms for enumerations with explicit stride values (CF #1087).
The currently-implemented syntax steals the identifiers
byanddownas new keywords; we should discuss if this is acceptable, or if new syntax should be designed.