diff --git a/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v b/saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v index 7e15985125..63512eb895 100644 --- 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 index 2df4e9fe22..6dd0b21a25 100644 --- 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;