From 3b82ee8d7de2033f9822fd9c7cadd96949662f7b Mon Sep 17 00:00:00 2001 From: Steve Zdancewic Date: Mon, 18 Mar 2024 13:43:33 -0400 Subject: [PATCH] missing axiom definition --- src/ml/extracted/ExtractFrontend.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ml/extracted/ExtractFrontend.v b/src/ml/extracted/ExtractFrontend.v index 159acff6..569d8ac3 100644 --- a/src/ml/extracted/ExtractFrontend.v +++ b/src/ml/extracted/ExtractFrontend.v @@ -55,5 +55,7 @@ Extract Constant randomRInt => "(fun (x,y) r -> let yint = coqZ2Int y in let xint = coqZ2Int x in if (yint < xint) then failwith ""choose called with unordered arguments"" else (int2CoqZ (xint + (Random.State.int r (yint - xint + 1))), r))". Extract Constant randomRN => "(fun (x,y) r -> let yint = coqN2Int y in let xint = coqN2Int x in if yint < xint then failwith ""choose called with unordered arguments"" else (int2CoqN (xint + (Random.State.int r (yint - xint + 1))), r))". +Extract Constant randomRNat => + "(fun (x,y) r -> let yint = ExtrOcamlIntConv.int_of_nat y in let xint = ExtrOcamlIntConv.int_of_nat x in if yint < xint then failwith ""choose called with unordered arguments"" else (ExtrOcamlIntConv.nat_of_int (xint + (Random.State.int r (yint - xint + 1))), r))". Separate Extraction LLVMAst AstLib TopLevel InterpretationStack ExtrOcamlIntConv ParserHelper ShowAST ReprAST GenAlive2.