From a714d4b1cc90089b80ac475f5b6882f05e98c355 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 25 Jan 2019 16:36:25 -0500 Subject: Support Nat.eqb in reification --- src/Language.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Language.v') diff --git a/src/Language.v b/src/Language.v index eba5cf85a..e4c5057db 100644 --- a/src/Language.v +++ b/src/Language.v @@ -855,6 +855,7 @@ Module Compilers. | Nat_mul : ident (nat -> nat -> nat) | Nat_add : ident (nat -> nat -> nat) | Nat_sub : ident (nat -> nat -> nat) + | Nat_eqb : ident (nat -> nat -> bool) | nil {t} : ident (list t) | cons {t:base.type} : ident (t -> list t -> list t) | pair {A B:base.type} : ident (A -> B -> A * B) @@ -995,6 +996,7 @@ Module Compilers. | Nat_mul => Nat.mul | Nat_add => Nat.add | Nat_sub => Nat.sub + | Nat_eqb => Nat.eqb | nil t => Datatypes.nil | cons t => Datatypes.cons | pair A B => Datatypes.pair -- cgit v1.2.3