Skip to content

Commit

Permalink
Eta-contract some definitions in Cryptol.sawcore.
Browse files Browse the repository at this point in the history
This should make it possible for `cryptol_ss` to simplify
things like `(<)` to `intLt` even when partially applied.
  • Loading branch information
Brian Huffman committed Feb 15, 2022
1 parent 44a38fb commit 583855d
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions cryptol-saw-core/saw/Cryptol.sawcore
Original file line number Diff line number Diff line change
Expand Up @@ -1154,20 +1154,20 @@ ecNotEq a pa x y = not (ecEq a pa x y);

-- Cmp
ecLt : (a : sort 0) -> PCmp a -> a -> a -> Bool;
ecLt a pa x y = pa.lt x y;
ecLt a pa = pa.lt;

ecGt : (a : sort 0) -> PCmp a -> a -> a -> Bool;
ecGt a pa x y = ecLt a pa y x;

ecLtEq : (a : sort 0) -> PCmp a -> a -> a -> Bool;
ecLtEq a pa x y = pa.le x y;
ecLtEq a pa = pa.le;

ecGtEq : (a : sort 0) -> PCmp a -> a -> a -> Bool;
ecGtEq a pa x y = ecLtEq a pa y x;

-- SignedCmp
ecSLt : (a : sort 0) -> PSignedCmp a -> a -> a -> Bool;
ecSLt a pa x y = pa.slt x y;
ecSLt a pa = pa.slt;

-- Logic
ecAnd : (a : sort 0) -> PLogic a -> a -> a -> a;
Expand Down

0 comments on commit 583855d

Please sign in to comment.