missing axiom definition

vellvm · Mar 18, 2024 · 3b82ee8 · 3b82ee8
1 parent f4947be
commit 3b82ee8
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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.