[isabelle] Questios about evaluation and code extraction
I am a beginner in Isabelle, and I have two (hopefully)
(1) Is it possible to evaluate, or normalize, terms inside Isabelle? I
know that one can exract executable specifications to ML ("Isabelle's
Logics: HOL", Section 2.9). I also know that in the proof mode I can
say apply(simp) to simplify, say, the goal "(12 :: int) div 5 = 2" to
True. But can I make Isabelle compute the result of "(12 :: int) div
(2) Is it possible to extract code from fragments that use rational
numbers? When I tried the following code:
constdefs f :: "rat => rat"
"f x == 1 / x + x"
code_module Inc file "rat.ml"
I got this error:
*** Unable to generate code for type:
*** 'a set
*** required by:
*** Quotient.quot (type), Rational.rat (type), <Top>
*** At command "code_module".
This archive was generated by a fusion of
Pipermail (Mailman edition) and