Email Gateway (Sep 10 2023 at 08:26): Email Gateway (Sep 10 2023 at 08:26):From: Guilherme Silva <guilhermegfsilva@gmail.com>
I'm trying to run the following code in Isabelle:
typedecl type_a
typedecl type_b
consts set_a :: "type_a set"
consts set_b :: "type_b set"
consts pairs :: "(type_a \<times> type_b) set"
definition func_1:: "bool" where
"func_1 \<equiv>
\<forall> a b .
((a, b) \<in> pairs \<longrightarrow> (a \<in> set_a \<and> b \<in>
set_b))"
export_code
func_1
in SML module_name SML_func_1
in Haskell module_name Haskell_func_1
in OCaml module_name OCaml_func_1
in Scala module_name Scala_func_1
But I get a "Wellsortedness error: Type type_a/type_b not of sort enum"
error when trying to export code because type_a and type_b are not defined
as enumerable types.
How do I define a new, enumerable type to bypass this? I was under the
impression that this was possible by using Enum.thy (
https://isabelle.in.tum.de/library/HOL/HOL/Enum.html), but I don't know how
exactly to use this theory to do this, or if there's another one than can
be used to do it.
Thanks,
G. Silva
Last updated: Apr 28 2024 at 20:16 UTC