From 7eadf3b3deaaedbcc3c51ffb55de03d37919c53b Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Fri, 11 Sep 2015 14:55:50 +0100
Subject: [PATCH] Lambda.v: nat_comparable was ok
---
generator/tests/lambda/Lambda.v | 2 --
generator/tests/lambda/LibNat.ml | 16 +++++++++++++++-
2 files changed, 15 insertions(+), 3 deletions(-)
diff --git a/generator/tests/lambda/Lambda.v b/generator/tests/lambda/Lambda.v
index 0ea183b..c29e4f4 100644
--- a/generator/tests/lambda/Lambda.v
+++ b/generator/tests/lambda/Lambda.v
@@ -129,8 +129,6 @@ Fixpoint run (n:nat) (t:trm) : res :=
(otherwise, useless errors will be launched). *)
Extraction Inline classicT LibEpsilon.Inhab_witness LibEpsilon.epsilon LibEpsilon.epsilon_def indefinite_description.
-Extract Constant nat_comparable => "(=)".
-
Set Extraction AccessOpaque.
Unset Extraction Optimize.
Unset Extraction KeepSingleton.
diff --git a/generator/tests/lambda/LibNat.ml b/generator/tests/lambda/LibNat.ml
index 67e6cc6..20e9a84 100644
--- a/generator/tests/lambda/LibNat.ml
+++ b/generator/tests/lambda/LibNat.ml
@@ -1,7 +1,21 @@
open Datatypes
open LibReflect
+(** val nat_compare : nat -> nat -> bool **)
+
+let rec nat_compare x y =
+ match x with
+ | O ->
+ (match y with
+ | O -> Coq_true
+ | S n -> Coq_false)
+ | S x' ->
+ (match y with
+ | O -> Coq_false
+ | S y' -> nat_compare x' y')
+
(** val nat_comparable : nat coq_Comparable **)
-let nat_comparable = (=)
+let nat_comparable x y =
+ nat_compare x y
--
GitLab