Re: [isabelle] Running a function defined in Isabelle
On 22/01/15 23:53, Bob Fang wrote:
Just wondering if I have defined a function in Isabelle, is there anyway to
write some simple test cases on my own first instead of jumping directly
into proving properties of it?
If you really want to do that, look into the code generator, which can
produce ML and Haskell (at least). It's an urge that I remember when
starting Isabelle, but after a while you tend to realise that you didn't
really need to do it.
Also, if I have proved a theorem, is it automatically added to the
rewriting rules or I have to add "[simp]:" in the theorem declaration?
No. Not all rules make safe (or even valid) rewriting rules. I
strongly recommend that you don't do this, unless you're absolutely
certain that you've got a safe and universally-useful simp rule.
This archive was generated by a fusion of
Pipermail (Mailman edition) and