Fix the SAWCore definition of maxNat.

Fixes #1502
GaloisInc · Nov 9, 2021 · d48769c · d48769c
1 parent b60d952
commit d48769c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v
@@ -420,7 +420,7 @@ Definition minNat : SAWCoreScaffolding.Nat -> SAWCoreScaffolding.Nat -> SAWCoreS
   fun (x : SAWCoreScaffolding.Nat) (y : SAWCoreScaffolding.Nat) => Nat_cases2 SAWCoreScaffolding.Nat (fun (y' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Zero) (fun (x' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Zero) (fun (x' : SAWCoreScaffolding.Nat) (y' : SAWCoreScaffolding.Nat) (min_xy : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ min_xy) x y.
 
 Definition maxNat : SAWCoreScaffolding.Nat -> SAWCoreScaffolding.Nat -> SAWCoreScaffolding.Nat :=
-  fun (x : SAWCoreScaffolding.Nat) (y : SAWCoreScaffolding.Nat) => Nat_cases2 SAWCoreScaffolding.Nat (fun (x' : SAWCoreScaffolding.Nat) => x') (fun (y' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ y') (fun (y' : SAWCoreScaffolding.Nat) (x' : SAWCoreScaffolding.Nat) (sub_xy : SAWCoreScaffolding.Nat) => sub_xy) y x.
+  fun (x : SAWCoreScaffolding.Nat) (y : SAWCoreScaffolding.Nat) => Nat_cases2 SAWCoreScaffolding.Nat (fun (y' : SAWCoreScaffolding.Nat) => y') (fun (x' : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ x') (fun (x' : SAWCoreScaffolding.Nat) (y' : SAWCoreScaffolding.Nat) (max_xy : SAWCoreScaffolding.Nat) => SAWCoreScaffolding.Succ max_xy) x y.
 
 (* Prelude.widthNat was skipped *)
 

diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore
@@ -859,9 +859,9 @@ minNat x y =
 -- | Maximum
 maxNat : Nat -> Nat -> Nat;
 maxNat x y =
-  Nat_cases2 Nat (\ (x':Nat) -> x')
-             (\ (y':Nat) -> Succ y')
-             (\ (y':Nat) -> \ (x':Nat) -> \ (sub_xy:Nat) -> sub_xy) y x;
+  Nat_cases2 Nat (\ (y':Nat) -> y')
+             (\ (x':Nat) -> Succ x')
+             (\ (x':Nat) -> \ (y':Nat) -> \ (max_xy:Nat) -> Succ max_xy) x y;
 
 -- | Width(n) = 1 + floor(log_2(n))
 primitive widthNat : Nat -> Nat;