小编tas*_*yPI的帖子

免责声明:我是伊莎贝尔的初学者.

我正在尝试使用"sqrt"将"sqrt"函数或函数和定义导出到Haskell.我的第一次尝试只是:

theory Scratch
   imports Complex_Main
begin
   definition val :: "real" where "val = sqrt 4"

   export_code val in Haskell 
end 

这导致以下错误:

Wellsortedness error
(in code equation root ?n ?x ?
              if equal_nat_inst.equal_nat ?n zero_nat_inst.zero_nat then zero_real_inst.zero_real
              else the_inv_into top_set_inst.top_set
                    (?y. times_real_inst.times_real (sgn_real_inst.sgn_real y)
                           (abs_real_inst.abs_real y ^ ?n))
                    ?x,
with dependency "val" -> "sqrt" -> "root"):
Type real not of sort {enum,equal}
No type arity real :: enum

所以我试图用Haskell的"Prelude.sqrt"替换"sqrt":

code_printing
  constant sqrt ? (Haskell) "Prelude.sqrt _"

export_code val in Haskell …