Skip to content

Commit 004862a

Browse files
author
Brian Huffman
committed
Eta-contract some definitions in Cryptol.sawcore.
This should make it possible for `cryptol_ss` to simplify things like `(<)` to `intLt` even when partially applied.
1 parent fc4c2a7 commit 004862a

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

cryptol-saw-core/saw/Cryptol.sawcore

+3-3
Original file line numberDiff line numberDiff line change
@@ -1154,20 +1154,20 @@ ecNotEq a pa x y = not (ecEq a pa x y);
11541154

11551155
-- Cmp
11561156
ecLt : (a : sort 0) -> PCmp a -> a -> a -> Bool;
1157-
ecLt a pa x y = pa.lt x y;
1157+
ecLt a pa = pa.lt;
11581158

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

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

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

11681168
-- SignedCmp
11691169
ecSLt : (a : sort 0) -> PSignedCmp a -> a -> a -> Bool;
1170-
ecSLt a pa x y = pa.slt x y;
1170+
ecSLt a pa = pa.slt;
11711171

11721172
-- Logic
11731173
ecAnd : (a : sort 0) -> PLogic a -> a -> a -> a;

0 commit comments

Comments
 (0)