Theory Tangent_Secant_Imperative_Test

theory Tangent_Secant_Imperative_Test
  imports Tangent_Numbers_Imperative Secant_Numbers_Imperative
begin

definition "tangent_number_imp n = 
  do {
    a ← tangent_numbers_imperative.compute_imp (nat_of_integer n);
    xs ← Array.freeze a;
    return (map integer_of_nat xs)
  }"

ML_val ‹@{code tangent_number_imp} 100 ()›


definition "secant_number_imp n = 
  do {
    a ← secant_numbers_imperative.compute_imp (nat_of_integer n);
    xs ← Array.freeze a;
    return (map integer_of_nat xs)
  }"

ML_val ‹@{code secant_number_imp} 100 ()›

end