[isabelle] No Code Equation for LIMSEQ



For technical reasons I am restricted at the moment to using Isabelle2009
I am trying to use code generation to generate code for trigonometric functions and other functions that utilize the real datatype.

I have the following code that is attempting to exercise this ability.

definition test_pi :: "real" where "test_pi = pi"
definition test_sin :: "real => real" where "test_sin x = sin x"
definition test_cos :: "real => real" where "test_cos x = cos x"
definition test_tan :: "real => real" where "test_tan x = tan x"
definition test_arcsin :: "real => real" where "test_arcsin x = arcsin x"
definition test_arccos :: "real => real" where "test_arccos x = arccos x"
definition test_arctan :: "real => real" where "test_arctan x = arctan x"
definition test_trig :: "real => real => real => real" where "test_trig x y a = cos (arctan (y / x) + sin a - pi/4)"

export_code
 test_pi test_sin test_cos test_tan
 test_arcsin test_arccos test_arctan
 test_trig
in OCaml
module_name "TestCodeGen"
file "TestCodeGen3.ml"

I am getting the following error message
### No code equation for LIMSEQ, The

Does anybody know where the code equations for LIMSEQ are defined?
I have looked through the HOL/Library but found nothing  so far.

Thank you for your time,
David Thayer





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.