Make it apparent (with Poly/ML for now) that Arbint.int = IntInf.int

HOL-Theorem-Prover · Oct 25, 2024 · e38b007 · e38b007
1 parent 729e1b5
commit e38b007
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/portableML/Arbint.sig b/src/portableML/Arbint.sig
@@ -1,7 +1,7 @@
 signature Arbint =
 sig
 
-  include Arbintcore where type int = Arbintcore.int
+  include Arbintcore
   val pp_int     : int -> HOLPP.pretty
 
 end
diff --git a/src/portableML/poly/Arbintcore.sig b/src/portableML/poly/Arbintcore.sig
@@ -1,7 +1,7 @@
 signature Arbintcore =
 sig
 
-  eqtype int
+  type int = IntInf.int
 
   type num = Arbnumcore.num