More predicate operators

[jldodds]

I would like to see syntactic sugar to allow all comparison operators (<, >, <=) in predicates

[brianhuffman]

I'm not sure what you mean; are you talking about something analogous to (===) and (!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit for the other comparisons?

[jldodds]

Maybe this is a documentation limitation, or maybe there's an ambiguity issue I hadn't considered. It'd be nice to write a type like

(fin n, fin x, n < x) => ...
instead of
(fin n, fin x, x-1 >= n)

[yav]

If we add the constraint synonyms that Brian suggested (which mostly requires us to pick a syntax, I think), we could just add synonyms for these to the Prelude. For example:

constraint x <= y = y >= x
etc.

[brianhuffman]

This could be accomplished with the proposed "constraint synonyms" feature (#373), if we extend it to allow infix operators.

[brianhuffman]

Pull request #627 will make it possible to add these definitions to the Cryptol prelude:

type constraint i > j = i >= j + 1
type constraint i < j = j >= i + 1